Entry Value
Package Name real-def
Count 10
Theorems
  • real_abs : !x. abs x = (if &0 <= x then x else --x)
  • real_div : !x y. ~(y = &0) ==> x / y = x * inv y
  • real_ge : !x y. x >= y <=> y <= x
  • real_gt : !x y. x > y <=> y < x
  • real_lt : !x y. x < y <=> ~(y <= x)
  • real_max : !m n. max m n = (if m <= n then n else m)
  • real_min : !m n. min m n = (if m <= n then m else n)
  • real_pow_suc : !x n. x pow SUC n = x * x pow n
  • real_pow_zero : !x. x pow 0 = &1
  • real_sub : !x y. x - y = x + --y
  • Back to main package page