Subversion Repositories wimsdev

!set methtit=Simple deduction of inequality
!set methenv=ZZ QQ RR
!set methparmtype=parm inequality >,\
        parm inequality <,choice 3,\
        function,choice 4,function
!set methparmrelax=1,2,3
!set methhelp=This method allows you to establish an implication between two\
 inequalities. This implication can be based on a composition of addition\
 of terms, transitivity with an obvious inequality, deduction between\
 strict and non-strict inequalities, and multiplication of two sides of an\
 inequality by a constant.\
 <p>\
 For example, it knows <p><center>\
   \( 2*x > -2 => -4*x < 10 - x ) .\
 </center> <p>\
 You can use this method either to weaken an inequality within the hypotheses,\
 or to strengthen one in the goal.

!if $wims_read_parm iswordof form check
 !goto $wims_read_parm
!endif

!set obj=!exec mathexp extract inequality\
$objects
!if $obj=$empty
 !set error1=no_object
 !set penalty1=1
 !exit
!endif
 
!exit
:form
 !set n1=!linecnt $mtobj1
 !set n2=!linecnt $mtobj2
 !if $methsubstep=1
  !if $n1<1
   !set methparm3=2
   !goto goal
  !endif
  !if $n2<1
   !set methparm3=1
   !goto ctx
  !endif
  :opt
  <b>$methtit.</b>
  $methhelp
  <p>
  Vous voulez&nbsp;:
  !formselect methparm3 list 0,1,2,3 prompt $ch_choose,\
        weaken an inequality in the hypotheses,\
        strengthen an inequality in the goal,\
        one hypothesis implies a goal
  !set methsubstep=2
 !else
  !bound methparm3 between integer 0 and 3 default 0
  !if $methparm3=0
   !goto opt
  !endif
  !if $methparm3 iswordof 1 3
   :ctx
   !set methparmrelax=2,3
   The inequality
   !read deduc/methparm.phtml 1
   implies
  !else
   :goal
   !set methparmrelax=1,3
   In order to prove
   !read deduc/methparm.phtml 2
   , it is enough to prove
  !endif 
  <br/> 
  !if $methparm3<3
   <input size=14 name=methparm4 value="$methparm4"/>
   !formselect methparm5 from 1 to 4 prompt <,>,<=,>=
   <input size=14 name=methparm6 value="$methparm6"/>
  !else
   !set methparmrelax=3,4,5,6
   !read deduc/methparm.phtml 2
  !endif
  !set methsubstep=1
 !endif
!exit
:check
 !bound $methparm3 between integer 0 and 2 default 0
 !if $methparm3=0
  error=empty_data
  !exit
 !endif
 pm3=$methparm3
 !if $methparm3=3
  pm3=1
  !distribute item $methparmobj2 into data,left2,sign2,right2
 !endif
 n=!linecnt $(mtobj$pm3)
 !if $(methparm$pm3)=0
  error=empty_data
  !exit
 !endif
 !distribute item $(methparmobj$pm3) into data,left1,sign1,right1
 oldineq=$left1 $sign1 $right1
 !distribute item >,<,= into gt,lt,eq
 !if $gt isin $sign1
  sign1=!translate internal $gt to $lt in $sign1
  !exchange left1,right1
 !endif
 !if $methparm3!=3
  left2=$methparm4
  sign2=!item $methparm5 of <,>,<=,>=
  right2=$methparm6
 !endif
 !read deduc/sub/simplify $left2 $sign2 $right2
 newineq=$out
 !if $gt isin $sign2
  sign2=!translate internal $gt to $lt in $sign2
  !exchange left2,right2
 !endif
 !if $pm3=2
  !exchange sign1,sign2
  !exchange left1,left2
  !exchange right1,right2
 !endif
 tester=($right1)-($left1)-($right2)+($left2)
 !if $eq isin $sign1 and $eq notin $sign2
  sign=<
 !else
  sign=<=
 !endif
 !read deduc/sub/checkineq $tester,$sign,0
 test=!word 1 of $out
 !if $test notwordof true false
  out=!exec maxima negsumdispflag:false;\
        expand($maximasimp(($right1)-($left1)));\
        expand($maximasimp(($right2)-($left2)));\
        negsumdispflag:true;
  !distribute lines $out into none,i1,i2
  out=!exec mathexp cut addition\
$i1\
$i2
  !distribute lines $out into t1,t2
  !distribute item $t1 into a1,a2,a3
  !distribute item $t2 into b1,b2,b3
  !if $a1=$empty
   a1=$a2 $a3
  !endif
  !if $b1=$empty
   b1=$b2 $b3
  !endif
  !read deduc/sub/checknumber ($a1)/($b1)
  !if $out notsametext true
   test=bad
  !else
   tester=($right1)-($left1)-(($a1)/($b1))*(($right2)-($left2))
   !read deduc/sub/checkineq $tester,$sign,0
   test=!word 1 of $out
  !endif
 !endif
 !if $test notwordof true false
  error=unjustified
  !if $methparm3=3
   !advance penalty
  !endif
  !exit
 !endif
 !if $test=false
  error=Your implication is not true!
  !advance penalty
  !exit
 !endif
 oldobject=$pm3
 newobject$pm3=$newineq
 methexp=!item $pm3 of Because \($oldineq),\
        Implies \($oldineq)
!exit