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