Subversion Repositories wimsdev

Rev

Rev 16135 | Blame | Compare with Previous | Last modification | View Log | RSS feed

!set methtit2=Multiply an inequality by an expression of constant sign
!set methtit=Multiply an inequality by an expression
!set methenv=ZZ QQ RR
!set methparmtype=function,parm inequality >,choice,parm inequality >
!set methparmrelax=4
!set methhelp=This method transforms an inequality \(A > B) to\
  \(A*f > B*f) (or \(A*f < B*f)), where \(f) is an algebraic expression of constant sign.\
  The method allows \(f) to have zeros. Due to this, there is not always\
  equivalence between the original inequality and the transformed one;\
  therefore it applies only on the hypotheses.

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

!exit
:form
 Multiply the inequality
!read deduc/methparm.phtml 2
 by the expression
!read deduc/methparm.phtml 1,10
 which is
!formselect methparm3 list 0,-1,1 prompt \
        $ch_choose, negative or zero, positive or zero
 because
!set ch_optional=it is a number
!read deduc/methparm.phtml 4
!exit
:check
!bound methparm3 within -1,0,1 default 0
!if $methparm3=0
  error=empty_data
  !exit
!endif
!distribute items $methparmobj2 into data,left,sign,right
!read deduc/sub/checkineq ($methparm1),=,0
ztest=$out
!if $ztest=true
  zr=zero
  sign2=>=
  !goto OK
!endif
!if $ztest=bad
  !if $methparm4<1
    :bad
    sens=!item ($methparm3+3)/2 of negative, positive
    error=I don't see why \($methparm1) is $sens.
    !exit
  !endif
  !distribute items $methparmobj4 into data,left2,sign2,right2
  gt=>
  lt=<
  eq=$(empty)=
  !if ($methparm3>0 and $lt isin $sign2) or \
          ($methparm3<0 and $gt isin $sign2)
    !exchange left2,right2
  !endif
  sens=!item ($methparm3+3)/2 of <,>
  !read deduc/sub/checkineq ($methparm1) - ($left2) + ($right2),$sens=,0\
        ($methparm1) - ($left2) + ($right2),=,0
  !distribute line $out into sn,zr
  !if $sn!=true
    !goto bad
  !endif
!else
  !if ($methparm1)*$methparm3<0
    error=Error of sign!
    !exit
  !endif
!endif
:OK
methexp=Multiply \($left $sign $right) by \($methparm1)

!read deduc/sub/simplify ($left) * ($methparm1)\
        ($right) * ($methparm1)
!distribute lines $out into newleft,newright
!if $newleft=$empty or $newright=$empty
  error=bad_data
  !exit
!endif
!if $methparm3<0
  newsign=!translate internal <> to >< in $sign
!else
  newsign=$sign
!endif
newobject2=$newleft $newsign $newright
!if $eq notin $sign and $zr=true and $eq isin $sign2
  newsign=$newsign=
  newobject0=$newobject2
  oldobject=0
!else
  oldobject=2
!endif

badsign=!translate internal <> to >< in $newsign
resultlist=$newobject2,\
        $newright $newsign $newleft,\
        $newleft $badsign $newright
!exit