2 reneeds "jordan/float.hl";;
4 Float.REAL_INEQUALITY_CALCULATOR [] `#3.1415 < #4.0 * atn (&1) /\ #4.0 * atn (&1) < #3.142`;;
6 Float.REAL_INEQUALITY_CALCULATOR [] `#1.26 < acs(#0.3) /\ acs (#0.3) < #1.27`;;
10 Float.REAL_INEQUALITY_CALCULATOR [] `#3.14159 < pi`;;
12 Float.INTERVAL_OF_TERM [] [] 5 `&7 + (\i. &i pow 2) 1`;;
14 Float.FLOAT_CONV `float (int_of_num 3) (int_of_num 20) <= float (int_of_num 3) (int_of_num 7) +. (float (int_of_num 4) (-- int_of_num 13))`;;
16 Float.FLOAT_LESS_CONV `&0 < float (int_of_num 3) (int_of_num 7) -. (float (int_of_num 4) (-- int_of_num 13))`;;
18 Float.REAL_INEQUALITY_CALCULATOR []
19 `-- (sum (0..1) (\i. (&i) pow 2)) < &1000`;;
21 Float.REAL_INEQUALITY_CALCULATOR []
24 let rjrj = new_definition `rjrj = sqrt(&3)`;;
26 Float.REAL_INEQUALITY_CALCULATOR [("rjrj",PURE_ONCE_REWRITE_CONV[rjrj])]
29 let jrjr = new_definition `jrjr x = sqrt(x)`;;
31 Float.REAL_INEQUALITY_CALCULATOR [("rjrj",PURE_ONCE_REWRITE_CONV[rjrj]);
32 ("jrjr",PURE_ONCE_REWRITE_CONV[jrjr])]
33 `#1.31607 < jrjr rjrj /\ jrjr rjrj < #1.31608`;;
35 Pervasives.sqrt(Pervasives.sqrt(3.0));;
37 let rkkk = new_definition `rkkk x y z = (x * y) pow 2 + z`;;
39 Float.REAL_INEQUALITY_CALCULATOR [("rkkk",PURE_ONCE_REWRITE_CONV[rkkk])]
40 `rkkk (&2) (&3) (&4) < #40.1`;;
42 Float.REAL_INEQUALITY_CALCULATOR []
43 `#0.019 < abs (&3 - #3.02)`;;
45 Float.REAL_INEQUALITY_CALCULATOR []
46 `pi + #0.019 < abs (&3 - #3.02)`;;
49 Float.REAL_INEQUALITY_CALCULATOR []
50 `sum (5..7) (\i. (&i) pow 2) < &1000`;;
52 Float.REAL_INEQUALITY_CALCULATOR [] `#12.91553 < #1.29155 pow 10 /\ #1.29155 pow 10 < #12.91554`;;
54 Float.REAL_INEQUALITY_CALCULATOR [] `#0.05 < &3 / (sqrt(&2) - #1.41)`;;
55 Float.REAL_INEQUALITY_CALCULATOR [] `#0.05 * #0.04 - #0.3 < &3 / (sqrt(&2) - #1.41)`;;
59 3.0 /. (Pervasives.sqrt(2.0) -. 1.0);;
61 Float.REAL_INEQUALITY_CALCULATOR [] `((\t. t + &1) #12.0) < #15.0 `;;
63 BETA_CONV `((\t. t + &1) #12.0)`;;
65 Float.REAL_INEQUALITY_CALCULATOR [] `-- ((\t. &t + &1) 3) < -- #3.0`;;
67 Float.REAL_INEQUALITY_CALCULATOR [] `#1.4142135 < sqrt(&2) /\ (sqrt(&2) < #1.4142136)`;;
69 Float.REAL_INEQUALITY_CALCULATOR []
70 `#4.059107977120 < sqrt(&7 / #3.2) + sqrt(&4 * sqrt(&2) + &1) /\
71 sqrt(&7 / #3.2) + sqrt(&4 * sqrt(&2) + &1)< #4.059107977121`;;
75 Float.REAL_INEQUALITY_CALCULATOR [] `sqrt( #0.001 ) < #0.00001`;;
77 Float.REAL_INEQUALITY_CALCULATOR [] `&1/ &0 < #0.00001`;;
78 Float.REAL_INEQUALITY_CALCULATOR []
79 `(\i. (&i) pow 2 + (&i)) 33 < &1000000`;;