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
 
-