Subversion Repositories wimsdev

Rev

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