Subversion Repositories wimsdev

condtest1=0

goal=!trim $m_goal

!if $goal=$empty

 goal=!trim $m_equivalence

 eqgoal=yes

!endif

!if $goal=$empty

 condtest1=1

 !exit

!endif

context=

cont=!nonempty lines $m_context

gt=>

lt=<

eq==

!if $gt isin $cont

 ff=!exec mathexp extract inequality\

$cont

 nn=!linecnt $ff

 !for n=1 to $nn

  l=!line $n of $ff

  !if $gt isin $l

   !distribute item $l into data,left,sign,right

   !distribute words $data into l_,s_,e_

   !if $sign iswordof $gt $gt$eq

    ss=!translate internal > to < in $sign

    new=$right $ss $left

    L=!line $l_ of $cont

    !reset l1,l2

    !if $s_>0

     l1=!char 1 to $s_ of $L

    !endif

    v_=!charcnt $L

    !if $e_<$v_

     l2=!char $e_+1 to -1 of $L

    !endif

    cont=!replace line number $l_ by $l1$new$l2 in $cont

   !endif

  !endif

 !next n 

!endif

n=!linecnt $cont

!if $n<1

 !if contradiction iswordof $m_goal

  condtest1=-1

 !endif

 !exit

!endif

!for i=1 to $n

 l=!line $i of $cont

 !if $i=1

  context=($l)

 !else

  context=$context And ($l)

 !endif

!next i

!if $context=$empty

# error=check_fail

 !exit

!endif

!if $gt isin $goal

 ff=!exec mathexp extract inequality\

$goal

 nn=!linecnt $ff

 !for n=1 to $nn

  l=!line $n of $ff

  !if $gt isin $l

   !distribute item $l into data,left,sign,right

   !distribute words $data into l_,s_,e_

   !if $sign iswordof $gt $gt$eq

    ss=!translate internal > to < in $sign

    new=$right $ss $left

    L=!line $l_ of $goal

    !reset l1,l2

    !if $s_>0

     l1=!char 1 to $s_ of $L

    !endif

    v_=!charcnt $L

    !if $e_<$v_

     l2=!char $e_+1 to -1 of $L

    !endif

    goal=!replace line number $l_ by $l1$new$l2 in $goal

   !endif

  !endif

 !next n 

!endif

goalcnt=!linecnt $goal

yinp=

!for i=1 to $goalcnt

 l=!line $i of $goal

 yinp=!append line CanProve(($context) => ($l)); to $yinp

!next i

yinp=!replace internal = by == in $yinp

yinp=!replace internal <== by <= in $yinp

yinp=!replace internal >== by >= in $yinp

yinp=!replace internal ==> by => in $yinp

out=!exec yacas $yinp

!if true notlineof $out and false notlineof $out

 !exit

!endif

!for i=1 to $goalcnt

 l=!line $i of $out

 !if $l issametext false

  condtest1=-1

  !exit

 !endif

 !if $l issametext true

  goal=!replace line number $i by $ in $goal

 !endif

!next i

goal=!nonempty lines $goal

goal=!trim $goal

!if $goal=$empty

 condtest1=1

 !exit

!endif

!if $eqgoal=yes

 m_equivalence=$goal

 m_goal=

!else

 m_goal=$goal

 m_equivalence=

!endif

!read deduc/objects.combine

!read deduc/objects.put $[$currstep-1]