reneeds "jordan/float.hl";;

Float.REAL_INEQUALITY_CALCULATOR []  `#3.1415 < #4.0 * atn  (&1) /\ #4.0 * atn (&1) < #3.142`;;

Float.REAL_INEQUALITY_CALCULATOR []  `#1.26 < acs(#0.3) /\ acs (#0.3) < #1.27`;;

acos (0.3);;

Float.REAL_INEQUALITY_CALCULATOR []  `#3.14159 < pi`;;

Float.INTERVAL_OF_TERM [] [] 5 `&7 + (\i. &i pow 2) 1`;;

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))`;;

Float.FLOAT_LESS_CONV `&0 <   float (int_of_num 3) (int_of_num 7) -. (float (int_of_num 4) (-- int_of_num 13))`;;

Float.REAL_INEQUALITY_CALCULATOR [] 
  `-- (sum (0..1) (\i. (&i) pow 2)) < &1000`;;

Float.REAL_INEQUALITY_CALCULATOR [] 
   `cos (&3) < pi`;;

let rjrj = new_definition `rjrj = sqrt(&3)`;;
Float.REAL_INEQUALITY_CALCULATOR [("rjrj",PURE_ONCE_REWRITE_CONV[rjrj])] 
   `rjrj < #1.73206`;;

let jrjr = new_definition `jrjr x = sqrt(x)`;;
Float.REAL_INEQUALITY_CALCULATOR [("rjrj",PURE_ONCE_REWRITE_CONV[rjrj]);
   ("jrjr",PURE_ONCE_REWRITE_CONV[jrjr])] 
   `#1.31607 < jrjr rjrj /\ jrjr rjrj < #1.31608`;;

Pervasives.sqrt(Pervasives.sqrt(3.0));;

let rkkk = new_definition `rkkk x y z = (x * y) pow 2 + z`;;
Float.REAL_INEQUALITY_CALCULATOR [("rkkk",PURE_ONCE_REWRITE_CONV[rkkk])] 
   `rkkk (&2) (&3) (&4) < #40.1`;;

Float.REAL_INEQUALITY_CALCULATOR [] 
  `#0.019 < abs (&3 - #3.02)`;;

Float.REAL_INEQUALITY_CALCULATOR [] 
  `pi + #0.019 < abs (&3 - #3.02)`;;


Float.REAL_INEQUALITY_CALCULATOR [] 
  `sum (5..7) (\i. (&i) pow 2) < &1000`;;

Float.REAL_INEQUALITY_CALCULATOR [] `#12.91553 < #1.29155 pow 10 /\ #1.29155 pow 10 < #12.91554`;;

Float.REAL_INEQUALITY_CALCULATOR [] `#0.05 < &3 / (sqrt(&2) - #1.41)`;;
Float.REAL_INEQUALITY_CALCULATOR [] `#0.05 * #0.04 - #0.3 < &3 / (sqrt(&2) - #1.41)`;;

Float.INTERVAL_DIV;;

3.0 /. (Pervasives.sqrt(2.0) -. 1.0);;

Float.REAL_INEQUALITY_CALCULATOR [] `((\t. t + &1) #12.0) < #15.0 `;;

BETA_CONV `((\t. t + &1) #12.0)`;;

Float.REAL_INEQUALITY_CALCULATOR [] `-- ((\t. &t + &1) 3) < -- #3.0`;;

Float.REAL_INEQUALITY_CALCULATOR [] `#1.4142135 < sqrt(&2) /\ (sqrt(&2) < #1.4142136)`;;

Float.REAL_INEQUALITY_CALCULATOR [] 
`#4.059107977120 < sqrt(&7 / #3.2) + sqrt(&4 * sqrt(&2) + &1) /\  
  sqrt(&7 / #3.2) + sqrt(&4 * sqrt(&2) + &1)< #4.059107977121`;;

Float.INTERVAL_DIV;;

Float.REAL_INEQUALITY_CALCULATOR [] `sqrt( #0.001 ) < #0.00001`;;

Float.REAL_INEQUALITY_CALCULATOR [] `&1/ &0  < #0.00001`;;
Float.REAL_INEQUALITY_CALCULATOR [] 
  `(\i. (&i) pow 2 + (&i)) 33 <  &1000000`;;