Subversion Repositories wimsdev

Rev

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 
 
 -