Go to most recent revision | Details | Last modification | View Log | RSS feed
Rev | Author | Line No. | Line |
---|---|---|---|
20 | reyssat | 1 | condtest1=0 |
2 | |||
3 | goal=!trim $m_goal |
||
4 | !if $goal=$empty |
||
5 | goal=!trim $m_equivalence |
||
6 | eqgoal=yes |
||
7 | !endif |
||
8 | |||
9 | !if $goal=$empty |
||
10 | condtest1=1 |
||
11 | !exit |
||
12 | !endif |
||
13 | |||
14 | context= |
||
15 | cont=!nonempty lines $m_context |
||
16 | gt=> |
||
17 | lt=< |
||
18 | eq== |
||
19 | !if $gt isin $cont |
||
20 | ff=!exec mathexp extract inequality\ |
||
21 | $cont |
||
22 | nn=!linecnt $ff |
||
23 | !for n=1 to $nn |
||
24 | l=!line $n of $ff |
||
25 | !if $gt isin $l |
||
26 | !distribute item $l into data,left,sign,right |
||
27 | !distribute words $data into l_,s_,e_ |
||
28 | !if $sign iswordof $gt $gt$eq |
||
29 | ss=!translate internal > to < in $sign |
||
30 | new=$right $ss $left |
||
31 | L=!line $l_ of $cont |
||
32 | !reset l1,l2 |
||
33 | !if $s_>0 |
||
34 | l1=!char 1 to $s_ of $L |
||
35 | !endif |
||
36 | v_=!charcnt $L |
||
37 | !if $e_<$v_ |
||
38 | l2=!char $e_+1 to -1 of $L |
||
39 | !endif |
||
40 | cont=!replace line number $l_ by $l1$new$l2 in $cont |
||
41 | !endif |
||
42 | !endif |
||
43 | !next n |
||
44 | !endif |
||
45 | n=!linecnt $cont |
||
46 | !if $n<1 |
||
47 | !if contradiction iswordof $m_goal |
||
48 | condtest1=-1 |
||
49 | !endif |
||
50 | !exit |
||
51 | !endif |
||
52 | !for i=1 to $n |
||
53 | l=!line $i of $cont |
||
54 | !if $i=1 |
||
55 | context=($l) |
||
56 | !else |
||
57 | context=$context And ($l) |
||
58 | !endif |
||
59 | !next i |
||
60 | |||
61 | !if $context=$empty |
||
62 | # error=check_fail |
||
63 | !exit |
||
64 | !endif |
||
65 | |||
66 | !if $gt isin $goal |
||
67 | ff=!exec mathexp extract inequality\ |
||
68 | $goal |
||
69 | nn=!linecnt $ff |
||
70 | !for n=1 to $nn |
||
71 | l=!line $n of $ff |
||
72 | !if $gt isin $l |
||
73 | !distribute item $l into data,left,sign,right |
||
74 | !distribute words $data into l_,s_,e_ |
||
75 | !if $sign iswordof $gt $gt$eq |
||
76 | ss=!translate internal > to < in $sign |
||
77 | new=$right $ss $left |
||
78 | L=!line $l_ of $goal |
||
79 | !reset l1,l2 |
||
80 | !if $s_>0 |
||
81 | l1=!char 1 to $s_ of $L |
||
82 | !endif |
||
83 | v_=!charcnt $L |
||
84 | !if $e_<$v_ |
||
85 | l2=!char $e_+1 to -1 of $L |
||
86 | !endif |
||
87 | goal=!replace line number $l_ by $l1$new$l2 in $goal |
||
88 | !endif |
||
89 | !endif |
||
90 | !next n |
||
91 | !endif |
||
92 | goalcnt=!linecnt $goal |
||
93 | yinp= |
||
94 | !for i=1 to $goalcnt |
||
95 | l=!line $i of $goal |
||
96 | yinp=!append line CanProve(($context) => ($l)); to $yinp |
||
97 | !next i |
||
98 | |||
99 | yinp=!replace internal = by == in $yinp |
||
100 | yinp=!replace internal <== by <= in $yinp |
||
101 | yinp=!replace internal >== by >= in $yinp |
||
102 | yinp=!replace internal ==> by => in $yinp |
||
103 | out=!exec yacas $yinp |
||
104 | |||
105 | !if true notlineof $out and false notlineof $out |
||
106 | !exit |
||
107 | !endif |
||
108 | |||
109 | !for i=1 to $goalcnt |
||
110 | l=!line $i of $out |
||
111 | !if $l issametext false |
||
112 | condtest1=-1 |
||
113 | !exit |
||
114 | !endif |
||
115 | !if $l issametext true |
||
116 | goal=!replace line number $i by $ in $goal |
||
117 | !endif |
||
118 | !next i |
||
119 | goal=!nonempty lines $goal |
||
120 | goal=!trim $goal |
||
121 | |||
122 | !if $goal=$empty |
||
123 | condtest1=1 |
||
124 | !exit |
||
125 | !endif |
||
126 | |||
127 | !if $eqgoal=yes |
||
128 | m_equivalence=$goal |
||
129 | m_goal= |
||
130 | !else |
||
131 | m_goal=$goal |
||
132 | m_equivalence= |
||
133 | !endif |
||
134 | |||
135 | !read deduc/objects.combine |
||
136 | !read deduc/objects.put $[$currstep-1] |
||
137 |