Subversion Repositories wimsdev

Rev

Rev 5763 | Go to most recent revision | Show entire file | Ignore whitespace | Details | Blame | Last modification | View Log | RSS feed

Rev 5763 Rev 16120
Line 9... Line 9...
9 
 The first two inequalities must already exist in the hypotheses, and the\
 9 
 The first two inequalities must already exist in the hypotheses, and the\
10 
 third will be added into the hypotheses. You can also give the two\
 10 
 third will be added into the hypotheses. You can also give the two\
11 
 original inequalities under the form \(A > B) and \(C < B) for example.
 11 
 original inequalities under the form \(A > B) and \(C < B) for example.
12 
 
 12 
 
13 
!if $wims_read_parm iswordof form check
 13 
!if $wims_read_parm iswordof form check
14 
 !goto $wims_read_parm
 14 
  !goto $wims_read_parm
15 
!endif
 15 
!endif
16 
 
 16 
 
17 
!exit
 17 
!exit
18 
:form
 18 
:form
19 
 Apply the transitivity on the inequalities
 19 
 Apply the transitivity on the inequalities
20 
 !read deduc/methparm.phtml 1
 20 
!read deduc/methparm.phtml 1
21 
 and
 21 
 and
22 
 !read deduc/methparm.phtml 2
 22 
!read deduc/methparm.phtml 2
23 
 
 23 
 
24 
!exit
 24 
!exit
25 
:check
 25 
:check
26 
 !distribute items $methparmobj1 into data,left1,sign1,right1
 26 
!distribute items $methparmobj1 into data,left1,sign1,right1
27 
 !distribute items $methparmobj2 into data,left2,sign2,right2
 27 
!distribute items $methparmobj2 into data,left2,sign2,right2
28 
 methexp=Transitivity on \($left1 $sign1 $right1) and \($left2 $sign2 $right2)
 28 
methexp=Transitivity on \($left1 $sign1 $right1) and \($left2 $sign2 $right2)
29
29 
 
30 
 gt=>
 30 
gt=>
31 
 lt=<
 31 
lt=<
32 
 !if ($gt isin $sign1 and $lt isin $sign2) or\
 32 
!if ($gt isin $sign1 and $lt isin $sign2) or\
33 
	($lt isin $sign1 and $gt isin $sign2)
 33 
	($lt isin $sign1 and $gt isin $sign2)
34 
  !exchange left2,right2
 34 
  !exchange left2,right2
35 
 !endif
 35 
!endif
36 
 !read deduc/sub/simplify ($right1) - ($left2)\
 36 
!read deduc/sub/simplify ($right1) - ($left2)\
37 
	($right2) - ($left1)
 37 
	($right2) - ($left1)
38 
 !distribute lines $out into test1,test2
 38 
!distribute lines $out into test1,test2
39 
 !if $test1!=0
 39 
!if $test1!=0
40 
  !if $test2!=0
 40 
  !if $test2!=0
41 
   error=The transitivity does not apply on your inequalities.
 41 
    error=The transitivity does not apply on your inequalities.
42 
   !advance penalty
 42 
    !advance penalty
43 
   !exit
 43 
    !exit
44 
  !else
 44 
  !else
45 
   !exchange right1,right2
 45 
    !exchange right1,right2
46 
   !exchange left1,left2
 46 
    !exchange left1,left2
47 
  !endif
 47 
  !endif
48 
 !endif
 48 
!endif
49 
 
 49 
 
50 
 !if $gt isin $sign1
 50 
!if $gt isin $sign1
51 
  s_=>
 51 
  s_=>
52 
 !else
 52 
!else
53 
  s_=<
 53 
  s_=<
54 
 !endif
 54 
!endif
55 
 eq=$empty=
 55 
eq=$empty=
56 
 !if $eq isin $sign1 and $eq isin $sign2
 56 
!if $eq isin $sign1 and $eq isin $sign2
57 
  s_=$s_=
 57 
  s_=$s_=
58 
 !endif
 58 
!endif
59 
 newobject0=$left1 $s_ $right2
 59 
newobject0=$left1 $s_ $right2
60 
 oldobject=0
 60 
oldobject=0
61 
 
 61 
 
62 
!exit
 62 
!exit
63 
 
 -