Structure realTheory


Source File Identifier index Theory binding index

signature realTheory =
sig
  type thm = Thm.thm

  (*  Definitions  *)
    val NUM_CEILING_def : thm
    val NUM_FLOOR_def : thm
    val abs : thm
    val inf_def : thm
    val max_def : thm
    val min_def : thm
    val pos_def : thm
    val pow : thm
    val real_div : thm
    val real_ge : thm
    val real_gt : thm
    val real_lte : thm
    val real_of_num : thm
    val real_sub : thm
    val sum_curried : thm
    val sum_tupled_primitive : thm
    val sup : thm

  (*  Theorems  *)
    val ABS_0 : thm
    val ABS_1 : thm
    val ABS_ABS : thm
    val ABS_BETWEEN : thm
    val ABS_BETWEEN1 : thm
    val ABS_BETWEEN2 : thm
    val ABS_BOUND : thm
    val ABS_BOUNDS : thm
    val ABS_CASES : thm
    val ABS_CIRCLE : thm
    val ABS_DIV : thm
    val ABS_INV : thm
    val ABS_LE : thm
    val ABS_LT_MUL2 : thm
    val ABS_MUL : thm
    val ABS_N : thm
    val ABS_NEG : thm
    val ABS_NZ : thm
    val ABS_POS : thm
    val ABS_POW2 : thm
    val ABS_REFL : thm
    val ABS_SIGN : thm
    val ABS_SIGN2 : thm
    val ABS_STILLNZ : thm
    val ABS_SUB : thm
    val ABS_SUB_ABS : thm
    val ABS_SUM : thm
    val ABS_TRIANGLE : thm
    val ABS_ZERO : thm
    val INFINITE_REAL_UNIV : thm
    val LE_NUM_CEILING : thm
    val NUM_CEILING_LE : thm
    val NUM_FLOOR_DIV : thm
    val NUM_FLOOR_DIV_LOWERBOUND : thm
    val NUM_FLOOR_EQNS : thm
    val NUM_FLOOR_LE : thm
    val NUM_FLOOR_LE2 : thm
    val NUM_FLOOR_LET : thm
    val NUM_FLOOR_LOWER_BOUND : thm
    val NUM_FLOOR_upper_bound : thm
    val POW_0 : thm
    val POW_1 : thm
    val POW_2 : thm
    val POW_2_LE1 : thm
    val POW_2_LT : thm
    val POW_ABS : thm
    val POW_ADD : thm
    val POW_EQ : thm
    val POW_INV : thm
    val POW_LE : thm
    val POW_LT : thm
    val POW_M1 : thm
    val POW_MINUS1 : thm
    val POW_MUL : thm
    val POW_NZ : thm
    val POW_ONE : thm
    val POW_PLUS1 : thm
    val POW_POS : thm
    val POW_POS_LT : thm
    val POW_ZERO : thm
    val POW_ZERO_EQ : thm
    val REAL : thm
    val REAL_0 : thm
    val REAL_1 : thm
    val REAL_10 : thm
    val REAL_ABS_0 : thm
    val REAL_ABS_MUL : thm
    val REAL_ABS_POS : thm
    val REAL_ABS_TRIANGLE : thm
    val REAL_ADD : thm
    val REAL_ADD2_SUB2 : thm
    val REAL_ADD_ASSOC : thm
    val REAL_ADD_COMM : thm
    val REAL_ADD_LDISTRIB : thm
    val REAL_ADD_LID : thm
    val REAL_ADD_LID_UNIQ : thm
    val REAL_ADD_LINV : thm
    val REAL_ADD_RAT : thm
    val REAL_ADD_RDISTRIB : thm
    val REAL_ADD_RID : thm
    val REAL_ADD_RID_UNIQ : thm
    val REAL_ADD_RINV : thm
    val REAL_ADD_SUB : thm
    val REAL_ADD_SUB2 : thm
    val REAL_ADD_SUB_ALT : thm
    val REAL_ADD_SYM : thm
    val REAL_ARCH : thm
    val REAL_ARCH_LEAST : thm
    val REAL_BIGNUM : thm
    val REAL_DIFFSQ : thm
    val REAL_DIV_ADD : thm
    val REAL_DIV_DENOM_CANCEL : thm
    val REAL_DIV_DENOM_CANCEL2 : thm
    val REAL_DIV_DENOM_CANCEL3 : thm
    val REAL_DIV_INNER_CANCEL : thm
    val REAL_DIV_INNER_CANCEL2 : thm
    val REAL_DIV_INNER_CANCEL3 : thm
    val REAL_DIV_LMUL : thm
    val REAL_DIV_LMUL_CANCEL : thm
    val REAL_DIV_LZERO : thm
    val REAL_DIV_MUL2 : thm
    val REAL_DIV_OUTER_CANCEL : thm
    val REAL_DIV_OUTER_CANCEL2 : thm
    val REAL_DIV_OUTER_CANCEL3 : thm
    val REAL_DIV_REFL : thm
    val REAL_DIV_REFL2 : thm
    val REAL_DIV_REFL3 : thm
    val REAL_DIV_RMUL : thm
    val REAL_DIV_RMUL_CANCEL : thm
    val REAL_DOUBLE : thm
    val REAL_DOWN : thm
    val REAL_DOWN2 : thm
    val REAL_ENTIRE : thm
    val REAL_EQ_IMP_LE : thm
    val REAL_EQ_LADD : thm
    val REAL_EQ_LDIV_EQ : thm
    val REAL_EQ_LMUL : thm
    val REAL_EQ_LMUL2 : thm
    val REAL_EQ_LMUL_IMP : thm
    val REAL_EQ_MUL_LCANCEL : thm
    val REAL_EQ_NEG : thm
    val REAL_EQ_RADD : thm
    val REAL_EQ_RDIV_EQ : thm
    val REAL_EQ_RMUL : thm
    val REAL_EQ_RMUL_IMP : thm
    val REAL_EQ_SUB_LADD : thm
    val REAL_EQ_SUB_RADD : thm
    val REAL_FACT_NZ : thm
    val REAL_HALF_BETWEEN : thm
    val REAL_HALF_DOUBLE : thm
    val REAL_IMP_INF_LE : thm
    val REAL_IMP_LE_INF : thm
    val REAL_IMP_LE_SUP : thm
    val REAL_IMP_MAX_LE2 : thm
    val REAL_IMP_MIN_LE2 : thm
    val REAL_IMP_SUP_LE : thm
    val REAL_INF_CLOSE : thm
    val REAL_INF_LE : thm
    val REAL_INF_LT : thm
    val REAL_INF_MIN : thm
    val REAL_INJ : thm
    val REAL_INV1 : thm
    val REAL_INVINV : thm
    val REAL_INV_0 : thm
    val REAL_INV_1OVER : thm
    val REAL_INV_EQ_0 : thm
    val REAL_INV_INJ : thm
    val REAL_INV_INV : thm
    val REAL_INV_LT1 : thm
    val REAL_INV_LT_ANTIMONO : thm
    val REAL_INV_MUL : thm
    val REAL_INV_NZ : thm
    val REAL_INV_POS : thm
    val REAL_LDISTRIB : thm
    val REAL_LE : thm
    val REAL_LE1_POW2 : thm
    val REAL_LET_ADD : thm
    val REAL_LET_ADD2 : thm
    val REAL_LET_ANTISYM : thm
    val REAL_LET_TOTAL : thm
    val REAL_LET_TRANS : thm
    val REAL_LE_01 : thm
    val REAL_LE_ADD : thm
    val REAL_LE_ADD2 : thm
    val REAL_LE_ADDL : thm
    val REAL_LE_ADDR : thm
    val REAL_LE_ANTISYM : thm
    val REAL_LE_DIV : thm
    val REAL_LE_DOUBLE : thm
    val REAL_LE_EPSILON : thm
    val REAL_LE_INV : thm
    val REAL_LE_INV_EQ : thm
    val REAL_LE_LADD : thm
    val REAL_LE_LADD_IMP : thm
    val REAL_LE_LDIV : thm
    val REAL_LE_LDIV_EQ : thm
    val REAL_LE_LMUL : thm
    val REAL_LE_LMUL_IMP : thm
    val REAL_LE_LNEG : thm
    val REAL_LE_LT : thm
    val REAL_LE_MAX : thm
    val REAL_LE_MAX1 : thm
    val REAL_LE_MAX2 : thm
    val REAL_LE_MIN : thm
    val REAL_LE_MUL : thm
    val REAL_LE_MUL2 : thm
    val REAL_LE_NEG : thm
    val REAL_LE_NEG2 : thm
    val REAL_LE_NEGL : thm
    val REAL_LE_NEGR : thm
    val REAL_LE_NEGTOTAL : thm
    val REAL_LE_POW2 : thm
    val REAL_LE_RADD : thm
    val REAL_LE_RDIV : thm
    val REAL_LE_RDIV_EQ : thm
    val REAL_LE_REFL : thm
    val REAL_LE_RMUL : thm
    val REAL_LE_RMUL_IMP : thm
    val REAL_LE_RNEG : thm
    val REAL_LE_SQUARE : thm
    val REAL_LE_SUB_CANCEL2 : thm
    val REAL_LE_SUB_LADD : thm
    val REAL_LE_SUB_RADD : thm
    val REAL_LE_SUP : thm
    val REAL_LE_TOTAL : thm
    val REAL_LE_TRANS : thm
    val REAL_LINV_UNIQ : thm
    val REAL_LIN_LE_MAX : thm
    val REAL_LNEG_UNIQ : thm
    val REAL_LT : thm
    val REAL_LT1_POW2 : thm
    val REAL_LTE_ADD : thm
    val REAL_LTE_ADD2 : thm
    val REAL_LTE_ANTSYM : thm
    val REAL_LTE_TOTAL : thm
    val REAL_LTE_TRANS : thm
    val REAL_LT_01 : thm
    val REAL_LT_1 : thm
    val REAL_LT_ADD : thm
    val REAL_LT_ADD1 : thm
    val REAL_LT_ADD2 : thm
    val REAL_LT_ADDL : thm
    val REAL_LT_ADDNEG : thm
    val REAL_LT_ADDNEG2 : thm
    val REAL_LT_ADDR : thm
    val REAL_LT_ADD_SUB : thm
    val REAL_LT_ANTISYM : thm
    val REAL_LT_DIV : thm
    val REAL_LT_FRACTION : thm
    val REAL_LT_FRACTION_0 : thm
    val REAL_LT_GT : thm
    val REAL_LT_HALF1 : thm
    val REAL_LT_HALF2 : thm
    val REAL_LT_IADD : thm
    val REAL_LT_IMP_LE : thm
    val REAL_LT_IMP_NE : thm
    val REAL_LT_INV : thm
    val REAL_LT_INV_EQ : thm
    val REAL_LT_LADD : thm
    val REAL_LT_LDIV_EQ : thm
    val REAL_LT_LE : thm
    val REAL_LT_LMUL : thm
    val REAL_LT_LMUL_0 : thm
    val REAL_LT_LMUL_IMP : thm
    val REAL_LT_MUL : thm
    val REAL_LT_MUL2 : thm
    val REAL_LT_MULTIPLE : thm
    val REAL_LT_NEG : thm
    val REAL_LT_NEGTOTAL : thm
    val REAL_LT_NZ : thm
    val REAL_LT_RADD : thm
    val REAL_LT_RDIV : thm
    val REAL_LT_RDIV_0 : thm
    val REAL_LT_RDIV_EQ : thm
    val REAL_LT_REFL : thm
    val REAL_LT_RMUL : thm
    val REAL_LT_RMUL_0 : thm
    val REAL_LT_RMUL_IMP : thm
    val REAL_LT_SUB_LADD : thm
    val REAL_LT_SUB_RADD : thm
    val REAL_LT_TOTAL : thm
    val REAL_LT_TRANS : thm
    val REAL_MAX_ADD : thm
    val REAL_MAX_ALT : thm
    val REAL_MAX_LE : thm
    val REAL_MAX_MIN : thm
    val REAL_MAX_REFL : thm
    val REAL_MAX_SUB : thm
    val REAL_MEAN : thm
    val REAL_MIDDLE1 : thm
    val REAL_MIDDLE2 : thm
    val REAL_MIN_ADD : thm
    val REAL_MIN_ALT : thm
    val REAL_MIN_LE : thm
    val REAL_MIN_LE1 : thm
    val REAL_MIN_LE2 : thm
    val REAL_MIN_LE_LIN : thm
    val REAL_MIN_MAX : thm
    val REAL_MIN_REFL : thm
    val REAL_MIN_SUB : thm
    val REAL_MUL : thm
    val REAL_MUL_ASSOC : thm
    val REAL_MUL_COMM : thm
    val REAL_MUL_LID : thm
    val REAL_MUL_LINV : thm
    val REAL_MUL_LNEG : thm
    val REAL_MUL_LZERO : thm
    val REAL_MUL_RID : thm
    val REAL_MUL_RINV : thm
    val REAL_MUL_RNEG : thm
    val REAL_MUL_RZERO : thm
    val REAL_MUL_SUB1_CANCEL : thm
    val REAL_MUL_SUB2_CANCEL : thm
    val REAL_MUL_SYM : thm
    val REAL_NEGNEG : thm
    val REAL_NEG_0 : thm
    val REAL_NEG_ADD : thm
    val REAL_NEG_EQ : thm
    val REAL_NEG_EQ0 : thm
    val REAL_NEG_GE0 : thm
    val REAL_NEG_GT0 : thm
    val REAL_NEG_HALF : thm
    val REAL_NEG_INV : thm
    val REAL_NEG_LE0 : thm
    val REAL_NEG_LMUL : thm
    val REAL_NEG_LT0 : thm
    val REAL_NEG_MINUS1 : thm
    val REAL_NEG_MUL2 : thm
    val REAL_NEG_NEG : thm
    val REAL_NEG_RMUL : thm
    val REAL_NEG_SUB : thm
    val REAL_NEG_THIRD : thm
    val REAL_NOT_LE : thm
    val REAL_NOT_LT : thm
    val REAL_NZ_IMP_LT : thm
    val REAL_OF_NUM_ADD : thm
    val REAL_OF_NUM_EQ : thm
    val REAL_OF_NUM_LE : thm
    val REAL_OF_NUM_MUL : thm
    val REAL_OF_NUM_POW : thm
    val REAL_OF_NUM_SUC : thm
    val REAL_OVER1 : thm
    val REAL_POASQ : thm
    val REAL_POS : thm
    val REAL_POS_EQ_ZERO : thm
    val REAL_POS_ID : thm
    val REAL_POS_INFLATE : thm
    val REAL_POS_LE_ZERO : thm
    val REAL_POS_MONO : thm
    val REAL_POS_NZ : thm
    val REAL_POS_POS : thm
    val REAL_POW2_ABS : thm
    val REAL_POW_ADD : thm
    val REAL_POW_DIV : thm
    val REAL_POW_INV : thm
    val REAL_POW_LT : thm
    val REAL_POW_LT2 : thm
    val REAL_POW_MONO_LT : thm
    val REAL_POW_POW : thm
    val REAL_RDISTRIB : thm
    val REAL_RINV_UNIQ : thm
    val REAL_RNEG_UNIQ : thm
    val REAL_SUB : thm
    val REAL_SUB_0 : thm
    val REAL_SUB_ABS : thm
    val REAL_SUB_ADD : thm
    val REAL_SUB_ADD2 : thm
    val REAL_SUB_INV2 : thm
    val REAL_SUB_LDISTRIB : thm
    val REAL_SUB_LE : thm
    val REAL_SUB_LNEG : thm
    val REAL_SUB_LT : thm
    val REAL_SUB_LZERO : thm
    val REAL_SUB_NEG2 : thm
    val REAL_SUB_RAT : thm
    val REAL_SUB_RDISTRIB : thm
    val REAL_SUB_REFL : thm
    val REAL_SUB_RNEG : thm
    val REAL_SUB_RZERO : thm
    val REAL_SUB_SUB : thm
    val REAL_SUB_SUB2 : thm
    val REAL_SUB_TRIANGLE : thm
    val REAL_SUMSQ : thm
    val REAL_SUP : thm
    val REAL_SUP_ALLPOS : thm
    val REAL_SUP_CONST : thm
    val REAL_SUP_EXISTS : thm
    val REAL_SUP_EXISTS_UNIQUE : thm
    val REAL_SUP_LE : thm
    val REAL_SUP_MAX : thm
    val REAL_SUP_SOMEPOS : thm
    val REAL_SUP_UBOUND : thm
    val REAL_SUP_UBOUND_LE : thm
    val REAL_THIRDS_BETWEEN : thm
    val SETOK_LE_LT : thm
    val SUM_0 : thm
    val SUM_1 : thm
    val SUM_2 : thm
    val SUM_ABS : thm
    val SUM_ABS_LE : thm
    val SUM_ADD : thm
    val SUM_BOUND : thm
    val SUM_CANCEL : thm
    val SUM_CMUL : thm
    val SUM_DIFF : thm
    val SUM_EQ : thm
    val SUM_GROUP : thm
    val SUM_LE : thm
    val SUM_NEG : thm
    val SUM_NSUB : thm
    val SUM_OFFSET : thm
    val SUM_PERMUTE_0 : thm
    val SUM_POS : thm
    val SUM_POS_GEN : thm
    val SUM_REINDEX : thm
    val SUM_SUB : thm
    val SUM_SUBST : thm
    val SUM_TWO : thm
    val SUM_ZERO : thm
    val SUP_EPSILON : thm
    val SUP_LEMMA1 : thm
    val SUP_LEMMA2 : thm
    val SUP_LEMMA3 : thm
    val add_ints : thm
    val add_rat : thm
    val add_ratl : thm
    val add_ratr : thm
    val div_rat : thm
    val div_ratl : thm
    val div_ratr : thm
    val eq_ints : thm
    val eq_rat : thm
    val eq_ratl : thm
    val eq_ratr : thm
    val le_int : thm
    val le_rat : thm
    val le_ratl : thm
    val le_ratr : thm
    val lt_int : thm
    val lt_rat : thm
    val lt_ratl : thm
    val lt_ratr : thm
    val mult_ints : thm
    val mult_rat : thm
    val mult_ratl : thm
    val mult_ratr : thm
    val neg_rat : thm
    val pow_rat : thm
    val real_lt : thm
    val sum : thm
    val sum_compute : thm
    val sum_ind : thm

  val real_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [realax] Parent theory of "real"

   [NUM_CEILING_def]  Definition

      |- ∀x. clg x = LEAST n. x ≤ &n

   [NUM_FLOOR_def]  Definition

      |- ∀x. flr x = LEAST n. &(n + 1) > x

   [abs]  Definition

      |- ∀x. abs x = if 0 ≤ x then x else -x

   [inf_def]  Definition

      |- ∀p. inf p = -sup (λr. p (-r))

   [max_def]  Definition

      |- ∀x y. max x y = if x ≤ y then y else x

   [min_def]  Definition

      |- ∀x y. min x y = if x ≤ y then x else y

   [pos_def]  Definition

      |- ∀x. pos x = if 0 ≤ x then x else 0

   [pow]  Definition

      |- (∀x. x pow 0 = 1) ∧ ∀x n. x pow SUC n = x * x pow n

   [real_div]  Definition

      |- ∀x y. x / y = x * inv y

   [real_ge]  Definition

      |- ∀x y. x ≥ y ⇔ y ≤ x

   [real_gt]  Definition

      |- ∀x y. x > y ⇔ y < x

   [real_lte]  Definition

      |- ∀x y. x ≤ y ⇔ ¬(y < x)

   [real_of_num]  Definition

      |- (0 = real_0) ∧ ∀n. &SUC n = &n + real_1

   [real_sub]  Definition

      |- ∀x y. x − y = x + -y

   [sum_curried]  Definition

      |- ∀x x1. sum x x1 = sum_tupled (x,x1)

   [sum_tupled_primitive]  Definition

      |- sum_tupled =
         WFREC (@R. WF R ∧ ∀f m n. R ((n,m),f) ((n,SUC m),f))
           (λsum_tupled a.
              case a of
                ((n,0),f) => I 0
              | ((n,SUC m),f) => I (sum_tupled ((n,m),f) + f (n + m)))

   [sup]  Definition

      |- ∀P. sup P = @s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s

   [ABS_0]  Theorem

      |- abs 0 = 0

   [ABS_1]  Theorem

      |- abs 1 = 1

   [ABS_ABS]  Theorem

      |- ∀x. abs (abs x) = abs x

   [ABS_BETWEEN]  Theorem

      |- ∀x y d. 0 < d ∧ x − d < y ∧ y < x + d ⇔ abs (y − x) < d

   [ABS_BETWEEN1]  Theorem

      |- ∀x y z. x < z ∧ abs (y − x) < z − x ⇒ y < z

   [ABS_BETWEEN2]  Theorem

      |- ∀x0 x y0 y.
           x0 < y0 ∧ abs (x − x0) < (y0 − x0) / 2 ∧
           abs (y − y0) < (y0 − x0) / 2 ⇒
           x < y

   [ABS_BOUND]  Theorem

      |- ∀x y d. abs (x − y) < d ⇒ y < x + d

   [ABS_BOUNDS]  Theorem

      |- ∀x k. abs x ≤ k ⇔ -k ≤ x ∧ x ≤ k

   [ABS_CASES]  Theorem

      |- ∀x. (x = 0) ∨ 0 < abs x

   [ABS_CIRCLE]  Theorem

      |- ∀x y h. abs h < abs y − abs x ⇒ abs (x + h) < abs y

   [ABS_DIV]  Theorem

      |- ∀y. y ≠ 0 ⇒ ∀x. abs (x / y) = abs x / abs y

   [ABS_INV]  Theorem

      |- ∀x. x ≠ 0 ⇒ (abs (inv x) = inv (abs x))

   [ABS_LE]  Theorem

      |- ∀x. x ≤ abs x

   [ABS_LT_MUL2]  Theorem

      |- ∀w x y z. abs w < y ∧ abs x < z ⇒ abs (w * x) < y * z

   [ABS_MUL]  Theorem

      |- ∀x y. abs (x * y) = abs x * abs y

   [ABS_N]  Theorem

      |- ∀n. abs (&n) = &n

   [ABS_NEG]  Theorem

      |- ∀x. abs (-x) = abs x

   [ABS_NZ]  Theorem

      |- ∀x. x ≠ 0 ⇔ 0 < abs x

   [ABS_POS]  Theorem

      |- ∀x. 0 ≤ abs x

   [ABS_POW2]  Theorem

      |- ∀x. abs (x pow 2) = x pow 2

   [ABS_REFL]  Theorem

      |- ∀x. (abs x = x) ⇔ 0 ≤ x

   [ABS_SIGN]  Theorem

      |- ∀x y. abs (x − y) < y ⇒ 0 < x

   [ABS_SIGN2]  Theorem

      |- ∀x y. abs (x − y) < -y ⇒ x < 0

   [ABS_STILLNZ]  Theorem

      |- ∀x y. abs (x − y) < abs y ⇒ x ≠ 0

   [ABS_SUB]  Theorem

      |- ∀x y. abs (x − y) = abs (y − x)

   [ABS_SUB_ABS]  Theorem

      |- ∀x y. abs (abs x − abs y) ≤ abs (x − y)

   [ABS_SUM]  Theorem

      |- ∀f m n. abs (sum (m,n) f) ≤ sum (m,n) (λn. abs (f n))

   [ABS_TRIANGLE]  Theorem

      |- ∀x y. abs (x + y) ≤ abs x + abs y

   [ABS_ZERO]  Theorem

      |- ∀x. (abs x = 0) ⇔ (x = 0)

   [INFINITE_REAL_UNIV]  Theorem

      |- INFINITE 𝕌(:real)

   [LE_NUM_CEILING]  Theorem

      |- ∀x. x ≤ &clg x

   [NUM_CEILING_LE]  Theorem

      |- ∀x n. x ≤ &n ⇒ clg x ≤ n

   [NUM_FLOOR_DIV]  Theorem

      |- 0 ≤ x ∧ 0 < y ⇒ &flr (x / y) * y ≤ x

   [NUM_FLOOR_DIV_LOWERBOUND]  Theorem

      |- 0 ≤ x ∧ 0 < y ⇒ x < &(flr (x / y) + 1) * y

   [NUM_FLOOR_EQNS]  Theorem

      |- (flr (&n) = n) ∧ (0 < m ⇒ (flr (&n / &m) = n DIV m))

   [NUM_FLOOR_LE]  Theorem

      |- 0 ≤ x ⇒ &flr x ≤ x

   [NUM_FLOOR_LE2]  Theorem

      |- 0 ≤ y ⇒ (x ≤ flr y ⇔ &x ≤ y)

   [NUM_FLOOR_LET]  Theorem

      |- flr x ≤ y ⇔ x < &y + 1

   [NUM_FLOOR_LOWER_BOUND]  Theorem

      |- x < &n ⇔ flr (x + 1) ≤ n

   [NUM_FLOOR_upper_bound]  Theorem

      |- &n ≤ x ⇔ n < flr (x + 1)

   [POW_0]  Theorem

      |- ∀n. 0 pow SUC n = 0

   [POW_1]  Theorem

      |- ∀x. x pow 1 = x

   [POW_2]  Theorem

      |- ∀x. x pow 2 = x * x

   [POW_2_LE1]  Theorem

      |- ∀n. 1 ≤ 2 pow n

   [POW_2_LT]  Theorem

      |- ∀n. &n < 2 pow n

   [POW_ABS]  Theorem

      |- ∀c n. abs c pow n = abs (c pow n)

   [POW_ADD]  Theorem

      |- ∀c m n. c pow (m + n) = c pow m * c pow n

   [POW_EQ]  Theorem

      |- ∀n x y. 0 ≤ x ∧ 0 ≤ y ∧ (x pow SUC n = y pow SUC n) ⇒ (x = y)

   [POW_INV]  Theorem

      |- ∀c. c ≠ 0 ⇒ ∀n. inv (c pow n) = inv c pow n

   [POW_LE]  Theorem

      |- ∀n x y. 0 ≤ x ∧ x ≤ y ⇒ x pow n ≤ y pow n

   [POW_LT]  Theorem

      |- ∀n x y. 0 ≤ x ∧ x < y ⇒ x pow SUC n < y pow SUC n

   [POW_M1]  Theorem

      |- ∀n. abs (-1 pow n) = 1

   [POW_MINUS1]  Theorem

      |- ∀n. -1 pow (2 * n) = 1

   [POW_MUL]  Theorem

      |- ∀n x y. (x * y) pow n = x pow n * y pow n

   [POW_NZ]  Theorem

      |- ∀c n. c ≠ 0 ⇒ c pow n ≠ 0

   [POW_ONE]  Theorem

      |- ∀n. 1 pow n = 1

   [POW_PLUS1]  Theorem

      |- ∀e. 0 < e ⇒ ∀n. 1 + &n * e ≤ (1 + e) pow n

   [POW_POS]  Theorem

      |- ∀x. 0 ≤ x ⇒ ∀n. 0 ≤ x pow n

   [POW_POS_LT]  Theorem

      |- ∀x n. 0 < x ⇒ 0 < x pow SUC n

   [POW_ZERO]  Theorem

      |- ∀n x. (x pow n = 0) ⇒ (x = 0)

   [POW_ZERO_EQ]  Theorem

      |- ∀n x. (x pow SUC n = 0) ⇔ (x = 0)

   [REAL]  Theorem

      |- ∀n. &SUC n = &n + 1

   [REAL_0]  Theorem

      |- real_0 = 0

   [REAL_1]  Theorem

      |- real_1 = 1

   [REAL_10]  Theorem

      |- 1 ≠ 0

   [REAL_ABS_0]  Theorem

      |- abs 0 = 0

   [REAL_ABS_MUL]  Theorem

      |- ∀x y. abs (x * y) = abs x * abs y

   [REAL_ABS_POS]  Theorem

      |- ∀x. 0 ≤ abs x

   [REAL_ABS_TRIANGLE]  Theorem

      |- ∀x y. abs (x + y) ≤ abs x + abs y

   [REAL_ADD]  Theorem

      |- ∀m n. &m + &n = &(m + n)

   [REAL_ADD2_SUB2]  Theorem

      |- ∀a b c d. a + b − (c + d) = a − c + (b − d)

   [REAL_ADD_ASSOC]  Theorem

      |- ∀x y z. x + (y + z) = x + y + z

   [REAL_ADD_COMM]  Theorem

      |- ∀x y. x + y = y + x

   [REAL_ADD_LDISTRIB]  Theorem

      |- ∀x y z. x * (y + z) = x * y + x * z

   [REAL_ADD_LID]  Theorem

      |- ∀x. 0 + x = x

   [REAL_ADD_LID_UNIQ]  Theorem

      |- ∀x y. (x + y = y) ⇔ (x = 0)

   [REAL_ADD_LINV]  Theorem

      |- ∀x. -x + x = 0

   [REAL_ADD_RAT]  Theorem

      |- ∀a b c d.
           b ≠ 0 ∧ d ≠ 0 ⇒ (a / b + c / d = (a * d + b * c) / (b * d))

   [REAL_ADD_RDISTRIB]  Theorem

      |- ∀x y z. (x + y) * z = x * z + y * z

   [REAL_ADD_RID]  Theorem

      |- ∀x. x + 0 = x

   [REAL_ADD_RID_UNIQ]  Theorem

      |- ∀x y. (x + y = x) ⇔ (y = 0)

   [REAL_ADD_RINV]  Theorem

      |- ∀x. x + -x = 0

   [REAL_ADD_SUB]  Theorem

      |- ∀x y. x + y − x = y

   [REAL_ADD_SUB2]  Theorem

      |- ∀x y. x − (x + y) = -y

   [REAL_ADD_SUB_ALT]  Theorem

      |- ∀x y. x + y − y = x

   [REAL_ADD_SYM]  Theorem

      |- ∀x y. x + y = y + x

   [REAL_ARCH]  Theorem

      |- ∀x. 0 < x ⇒ ∀y. ∃n. y < &n * x

   [REAL_ARCH_LEAST]  Theorem

      |- ∀y. 0 < y ⇒ ∀x. 0 ≤ x ⇒ ∃n. &n * y ≤ x ∧ x < &SUC n * y

   [REAL_BIGNUM]  Theorem

      |- ∀r. ∃n. r < &n

   [REAL_DIFFSQ]  Theorem

      |- ∀x y. (x + y) * (x − y) = x * x − y * y

   [REAL_DIV_ADD]  Theorem

      |- ∀x y z. y / x + z / x = (y + z) / x

   [REAL_DIV_DENOM_CANCEL]  Theorem

      |- ∀x y z. x ≠ 0 ⇒ (y / x / (z / x) = y / z)

   [REAL_DIV_DENOM_CANCEL2]  Theorem

      |- ∀y z. y / 2 / (z / 2) = y / z

   [REAL_DIV_DENOM_CANCEL3]  Theorem

      |- ∀y z. y / 3 / (z / 3) = y / z

   [REAL_DIV_INNER_CANCEL]  Theorem

      |- ∀x y z. x ≠ 0 ⇒ (y / x * (x / z) = y / z)

   [REAL_DIV_INNER_CANCEL2]  Theorem

      |- ∀y z. y / 2 * (2 / z) = y / z

   [REAL_DIV_INNER_CANCEL3]  Theorem

      |- ∀y z. y / 3 * (3 / z) = y / z

   [REAL_DIV_LMUL]  Theorem

      |- ∀x y. y ≠ 0 ⇒ (y * (x / y) = x)

   [REAL_DIV_LMUL_CANCEL]  Theorem

      |- ∀c a b. c ≠ 0 ⇒ (c * a / (c * b) = a / b)

   [REAL_DIV_LZERO]  Theorem

      |- ∀x. 0 / x = 0

   [REAL_DIV_MUL2]  Theorem

      |- ∀x z. x ≠ 0 ∧ z ≠ 0 ⇒ ∀y. y / z = x * y / (x * z)

   [REAL_DIV_OUTER_CANCEL]  Theorem

      |- ∀x y z. x ≠ 0 ⇒ (x / y * (z / x) = z / y)

   [REAL_DIV_OUTER_CANCEL2]  Theorem

      |- ∀y z. 2 / y * (z / 2) = z / y

   [REAL_DIV_OUTER_CANCEL3]  Theorem

      |- ∀y z. 3 / y * (z / 3) = z / y

   [REAL_DIV_REFL]  Theorem

      |- ∀x. x ≠ 0 ⇒ (x / x = 1)

   [REAL_DIV_REFL2]  Theorem

      |- 2 / 2 = 1

   [REAL_DIV_REFL3]  Theorem

      |- 3 / 3 = 1

   [REAL_DIV_RMUL]  Theorem

      |- ∀x y. y ≠ 0 ⇒ (x / y * y = x)

   [REAL_DIV_RMUL_CANCEL]  Theorem

      |- ∀c a b. c ≠ 0 ⇒ (a * c / (b * c) = a / b)

   [REAL_DOUBLE]  Theorem

      |- ∀x. x + x = 2 * x

   [REAL_DOWN]  Theorem

      |- ∀x. 0 < x ⇒ ∃y. 0 < y ∧ y < x

   [REAL_DOWN2]  Theorem

      |- ∀x y. 0 < x ∧ 0 < y ⇒ ∃z. 0 < z ∧ z < x ∧ z < y

   [REAL_ENTIRE]  Theorem

      |- ∀x y. (x * y = 0) ⇔ (x = 0) ∨ (y = 0)

   [REAL_EQ_IMP_LE]  Theorem

      |- ∀x y. (x = y) ⇒ x ≤ y

   [REAL_EQ_LADD]  Theorem

      |- ∀x y z. (x + y = x + z) ⇔ (y = z)

   [REAL_EQ_LDIV_EQ]  Theorem

      |- ∀x y z. 0 < z ⇒ ((x / z = y) ⇔ (x = y * z))

   [REAL_EQ_LMUL]  Theorem

      |- ∀x y z. (x * y = x * z) ⇔ (x = 0) ∨ (y = z)

   [REAL_EQ_LMUL2]  Theorem

      |- ∀x y z. x ≠ 0 ⇒ ((y = z) ⇔ (x * y = x * z))

   [REAL_EQ_LMUL_IMP]  Theorem

      |- ∀x y z. x ≠ 0 ∧ (x * y = x * z) ⇒ (y = z)

   [REAL_EQ_MUL_LCANCEL]  Theorem

      |- ∀x y z. (x * y = x * z) ⇔ (x = 0) ∨ (y = z)

   [REAL_EQ_NEG]  Theorem

      |- ∀x y. (-x = -y) ⇔ (x = y)

   [REAL_EQ_RADD]  Theorem

      |- ∀x y z. (x + z = y + z) ⇔ (x = y)

   [REAL_EQ_RDIV_EQ]  Theorem

      |- ∀x y z. 0 < z ⇒ ((x = y / z) ⇔ (x * z = y))

   [REAL_EQ_RMUL]  Theorem

      |- ∀x y z. (x * z = y * z) ⇔ (z = 0) ∨ (x = y)

   [REAL_EQ_RMUL_IMP]  Theorem

      |- ∀x y z. z ≠ 0 ∧ (x * z = y * z) ⇒ (x = y)

   [REAL_EQ_SUB_LADD]  Theorem

      |- ∀x y z. (x = y − z) ⇔ (x + z = y)

   [REAL_EQ_SUB_RADD]  Theorem

      |- ∀x y z. (x − y = z) ⇔ (x = z + y)

   [REAL_FACT_NZ]  Theorem

      |- ∀n. &FACT n ≠ 0

   [REAL_HALF_BETWEEN]  Theorem

      |- (0 < 1 / 2 ∧ 1 / 2 < 1) ∧ 0 ≤ 1 / 2 ∧ 1 / 2 ≤ 1

   [REAL_HALF_DOUBLE]  Theorem

      |- ∀x. x / 2 + x / 2 = x

   [REAL_IMP_INF_LE]  Theorem

      |- ∀p r. (∃z. ∀x. p x ⇒ z ≤ x) ∧ (∃x. p x ∧ x ≤ r) ⇒ inf p ≤ r

   [REAL_IMP_LE_INF]  Theorem

      |- ∀p r. (∃x. p x) ∧ (∀x. p x ⇒ r ≤ x) ⇒ r ≤ inf p

   [REAL_IMP_LE_SUP]  Theorem

      |- ∀p x.
           (∃r. p r) ∧ (∃z. ∀r. p r ⇒ r ≤ z) ∧ (∃r. p r ∧ x ≤ r) ⇒
           x ≤ sup p

   [REAL_IMP_MAX_LE2]  Theorem

      |- ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ max x1 x2 ≤ max y1 y2

   [REAL_IMP_MIN_LE2]  Theorem

      |- ∀x1 x2 y1 y2. x1 ≤ y1 ∧ x2 ≤ y2 ⇒ min x1 x2 ≤ min y1 y2

   [REAL_IMP_SUP_LE]  Theorem

      |- ∀p x. (∃r. p r) ∧ (∀r. p r ⇒ r ≤ x) ⇒ sup p ≤ x

   [REAL_INF_CLOSE]  Theorem

      |- ∀p e. (∃x. p x) ∧ 0 < e ⇒ ∃x. p x ∧ x < inf p + e

   [REAL_INF_LE]  Theorem

      |- ∀p x.
           (∃y. p y) ∧ (∃y. ∀z. p z ⇒ y ≤ z) ⇒
           (inf p ≤ x ⇔ ∀y. (∀z. p z ⇒ y ≤ z) ⇒ y ≤ x)

   [REAL_INF_LT]  Theorem

      |- ∀p z. (∃x. p x) ∧ inf p < z ⇒ ∃x. p x ∧ x < z

   [REAL_INF_MIN]  Theorem

      |- ∀p z. p z ∧ (∀x. p x ⇒ z ≤ x) ⇒ (inf p = z)

   [REAL_INJ]  Theorem

      |- ∀m n. (&m = &n) ⇔ (m = n)

   [REAL_INV1]  Theorem

      |- inv 1 = 1

   [REAL_INVINV]  Theorem

      |- ∀x. x ≠ 0 ⇒ (inv (inv x) = x)

   [REAL_INV_0]  Theorem

      |- inv 0 = 0

   [REAL_INV_1OVER]  Theorem

      |- ∀x. inv x = 1 / x

   [REAL_INV_EQ_0]  Theorem

      |- ∀x. (inv x = 0) ⇔ (x = 0)

   [REAL_INV_INJ]  Theorem

      |- ∀x y. (inv x = inv y) ⇔ (x = y)

   [REAL_INV_INV]  Theorem

      |- ∀x. inv (inv x) = x

   [REAL_INV_LT1]  Theorem

      |- ∀x. 0 < x ∧ x < 1 ⇒ 1 < inv x

   [REAL_INV_LT_ANTIMONO]  Theorem

      |- ∀x y. 0 < x ∧ 0 < y ⇒ (inv x < inv y ⇔ y < x)

   [REAL_INV_MUL]  Theorem

      |- ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (inv (x * y) = inv x * inv y)

   [REAL_INV_NZ]  Theorem

      |- ∀x. x ≠ 0 ⇒ inv x ≠ 0

   [REAL_INV_POS]  Theorem

      |- ∀x. 0 < x ⇒ 0 < inv x

   [REAL_LDISTRIB]  Theorem

      |- ∀x y z. x * (y + z) = x * y + x * z

   [REAL_LE]  Theorem

      |- ∀m n. &m ≤ &n ⇔ m ≤ n

   [REAL_LE1_POW2]  Theorem

      |- ∀x. 1 ≤ x ⇒ 1 ≤ x pow 2

   [REAL_LET_ADD]  Theorem

      |- ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y

   [REAL_LET_ADD2]  Theorem

      |- ∀w x y z. w ≤ x ∧ y < z ⇒ w + y < x + z

   [REAL_LET_ANTISYM]  Theorem

      |- ∀x y. ¬(x < y ∧ y ≤ x)

   [REAL_LET_TOTAL]  Theorem

      |- ∀x y. x ≤ y ∨ y < x

   [REAL_LET_TRANS]  Theorem

      |- ∀x y z. x ≤ y ∧ y < z ⇒ x < z

   [REAL_LE_01]  Theorem

      |- 0 ≤ 1

   [REAL_LE_ADD]  Theorem

      |- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y

   [REAL_LE_ADD2]  Theorem

      |- ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z

   [REAL_LE_ADDL]  Theorem

      |- ∀x y. y ≤ x + y ⇔ 0 ≤ x

   [REAL_LE_ADDR]  Theorem

      |- ∀x y. x ≤ x + y ⇔ 0 ≤ y

   [REAL_LE_ANTISYM]  Theorem

      |- ∀x y. x ≤ y ∧ y ≤ x ⇔ (x = y)

   [REAL_LE_DIV]  Theorem

      |- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x / y

   [REAL_LE_DOUBLE]  Theorem

      |- ∀x. 0 ≤ x + x ⇔ 0 ≤ x

   [REAL_LE_EPSILON]  Theorem

      |- ∀x y. (∀e. 0 < e ⇒ x ≤ y + e) ⇒ x ≤ y

   [REAL_LE_INV]  Theorem

      |- ∀x. 0 ≤ x ⇒ 0 ≤ inv x

   [REAL_LE_INV_EQ]  Theorem

      |- ∀x. 0 ≤ inv x ⇔ 0 ≤ x

   [REAL_LE_LADD]  Theorem

      |- ∀x y z. x + y ≤ x + z ⇔ y ≤ z

   [REAL_LE_LADD_IMP]  Theorem

      |- ∀x y z. y ≤ z ⇒ x + y ≤ x + z

   [REAL_LE_LDIV]  Theorem

      |- ∀x y z. 0 < x ∧ y ≤ z * x ⇒ y / x ≤ z

   [REAL_LE_LDIV_EQ]  Theorem

      |- ∀x y z. 0 < z ⇒ (x / z ≤ y ⇔ x ≤ y * z)

   [REAL_LE_LMUL]  Theorem

      |- ∀x y z. 0 < x ⇒ (x * y ≤ x * z ⇔ y ≤ z)

   [REAL_LE_LMUL_IMP]  Theorem

      |- ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ x * y ≤ x * z

   [REAL_LE_LNEG]  Theorem

      |- ∀x y. -x ≤ y ⇔ 0 ≤ x + y

   [REAL_LE_LT]  Theorem

      |- ∀x y. x ≤ y ⇔ x < y ∨ (x = y)

   [REAL_LE_MAX]  Theorem

      |- ∀z x y. z ≤ max x y ⇔ z ≤ x ∨ z ≤ y

   [REAL_LE_MAX1]  Theorem

      |- ∀x y. x ≤ max x y

   [REAL_LE_MAX2]  Theorem

      |- ∀x y. y ≤ max x y

   [REAL_LE_MIN]  Theorem

      |- ∀z x y. z ≤ min x y ⇔ z ≤ x ∧ z ≤ y

   [REAL_LE_MUL]  Theorem

      |- ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y

   [REAL_LE_MUL2]  Theorem

      |- ∀x1 x2 y1 y2.
           0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 ≤ x2 ∧ y1 ≤ y2 ⇒ x1 * y1 ≤ x2 * y2

   [REAL_LE_NEG]  Theorem

      |- ∀x y. -x ≤ -y ⇔ y ≤ x

   [REAL_LE_NEG2]  Theorem

      |- ∀x y. -x ≤ -y ⇔ y ≤ x

   [REAL_LE_NEGL]  Theorem

      |- ∀x. -x ≤ x ⇔ 0 ≤ x

   [REAL_LE_NEGR]  Theorem

      |- ∀x. x ≤ -x ⇔ x ≤ 0

   [REAL_LE_NEGTOTAL]  Theorem

      |- ∀x. 0 ≤ x ∨ 0 ≤ -x

   [REAL_LE_POW2]  Theorem

      |- ∀x. 0 ≤ x pow 2

   [REAL_LE_RADD]  Theorem

      |- ∀x y z. x + z ≤ y + z ⇔ x ≤ y

   [REAL_LE_RDIV]  Theorem

      |- ∀x y z. 0 < x ∧ y * x ≤ z ⇒ y ≤ z / x

   [REAL_LE_RDIV_EQ]  Theorem

      |- ∀x y z. 0 < z ⇒ (x ≤ y / z ⇔ x * z ≤ y)

   [REAL_LE_REFL]  Theorem

      |- ∀x. x ≤ x

   [REAL_LE_RMUL]  Theorem

      |- ∀x y z. 0 < z ⇒ (x * z ≤ y * z ⇔ x ≤ y)

   [REAL_LE_RMUL_IMP]  Theorem

      |- ∀x y z. 0 ≤ x ∧ y ≤ z ⇒ y * x ≤ z * x

   [REAL_LE_RNEG]  Theorem

      |- ∀x y. x ≤ -y ⇔ x + y ≤ 0

   [REAL_LE_SQUARE]  Theorem

      |- ∀x. 0 ≤ x * x

   [REAL_LE_SUB_CANCEL2]  Theorem

      |- ∀x y z. x − z ≤ y − z ⇔ x ≤ y

   [REAL_LE_SUB_LADD]  Theorem

      |- ∀x y z. x ≤ y − z ⇔ x + z ≤ y

   [REAL_LE_SUB_RADD]  Theorem

      |- ∀x y z. x − y ≤ z ⇔ x ≤ z + y

   [REAL_LE_SUP]  Theorem

      |- ∀p x.
           (∃y. p y) ∧ (∃y. ∀z. p z ⇒ z ≤ y) ⇒
           (x ≤ sup p ⇔ ∀y. (∀z. p z ⇒ z ≤ y) ⇒ x ≤ y)

   [REAL_LE_TOTAL]  Theorem

      |- ∀x y. x ≤ y ∨ y ≤ x

   [REAL_LE_TRANS]  Theorem

      |- ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z

   [REAL_LINV_UNIQ]  Theorem

      |- ∀x y. (x * y = 1) ⇒ (x = inv y)

   [REAL_LIN_LE_MAX]  Theorem

      |- ∀z x y. 0 ≤ z ∧ z ≤ 1 ⇒ z * x + (1 − z) * y ≤ max x y

   [REAL_LNEG_UNIQ]  Theorem

      |- ∀x y. (x + y = 0) ⇔ (x = -y)

   [REAL_LT]  Theorem

      |- ∀m n. &m < &n ⇔ m < n

   [REAL_LT1_POW2]  Theorem

      |- ∀x. 1 < x ⇒ 1 < x pow 2

   [REAL_LTE_ADD]  Theorem

      |- ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y

   [REAL_LTE_ADD2]  Theorem

      |- ∀w x y z. w < x ∧ y ≤ z ⇒ w + y < x + z

   [REAL_LTE_ANTSYM]  Theorem

      |- ∀x y. ¬(x ≤ y ∧ y < x)

   [REAL_LTE_TOTAL]  Theorem

      |- ∀x y. x < y ∨ y ≤ x

   [REAL_LTE_TRANS]  Theorem

      |- ∀x y z. x < y ∧ y ≤ z ⇒ x < z

   [REAL_LT_01]  Theorem

      |- 0 < 1

   [REAL_LT_1]  Theorem

      |- ∀x y. 0 ≤ x ∧ x < y ⇒ x / y < 1

   [REAL_LT_ADD]  Theorem

      |- ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y

   [REAL_LT_ADD1]  Theorem

      |- ∀x y. x ≤ y ⇒ x < y + 1

   [REAL_LT_ADD2]  Theorem

      |- ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z

   [REAL_LT_ADDL]  Theorem

      |- ∀x y. y < x + y ⇔ 0 < x

   [REAL_LT_ADDNEG]  Theorem

      |- ∀x y z. y < x + -z ⇔ y + z < x

   [REAL_LT_ADDNEG2]  Theorem

      |- ∀x y z. x + -y < z ⇔ x < z + y

   [REAL_LT_ADDR]  Theorem

      |- ∀x y. x < x + y ⇔ 0 < y

   [REAL_LT_ADD_SUB]  Theorem

      |- ∀x y z. x + y < z ⇔ x < z − y

   [REAL_LT_ANTISYM]  Theorem

      |- ∀x y. ¬(x < y ∧ y < x)

   [REAL_LT_DIV]  Theorem

      |- ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x / y

   [REAL_LT_FRACTION]  Theorem

      |- ∀n d. 1 < n ⇒ (d / &n < d ⇔ 0 < d)

   [REAL_LT_FRACTION_0]  Theorem

      |- ∀n d. n ≠ 0 ⇒ (0 < d / &n ⇔ 0 < d)

   [REAL_LT_GT]  Theorem

      |- ∀x y. x < y ⇒ ¬(y < x)

   [REAL_LT_HALF1]  Theorem

      |- ∀d. 0 < d / 2 ⇔ 0 < d

   [REAL_LT_HALF2]  Theorem

      |- ∀d. d / 2 < d ⇔ 0 < d

   [REAL_LT_IADD]  Theorem

      |- ∀x y z. y < z ⇒ x + y < x + z

   [REAL_LT_IMP_LE]  Theorem

      |- ∀x y. x < y ⇒ x ≤ y

   [REAL_LT_IMP_NE]  Theorem

      |- ∀x y. x < y ⇒ x ≠ y

   [REAL_LT_INV]  Theorem

      |- ∀x y. 0 < x ∧ x < y ⇒ inv y < inv x

   [REAL_LT_INV_EQ]  Theorem

      |- ∀x. 0 < inv x ⇔ 0 < x

   [REAL_LT_LADD]  Theorem

      |- ∀x y z. x + y < x + z ⇔ y < z

   [REAL_LT_LDIV_EQ]  Theorem

      |- ∀x y z. 0 < z ⇒ (x / z < y ⇔ x < y * z)

   [REAL_LT_LE]  Theorem

      |- ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y

   [REAL_LT_LMUL]  Theorem

      |- ∀x y z. 0 < x ⇒ (x * y < x * z ⇔ y < z)

   [REAL_LT_LMUL_0]  Theorem

      |- ∀x y. 0 < x ⇒ (0 < x * y ⇔ 0 < y)

   [REAL_LT_LMUL_IMP]  Theorem

      |- ∀x y z. y < z ∧ 0 < x ⇒ x * y < x * z

   [REAL_LT_MUL]  Theorem

      |- ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x * y

   [REAL_LT_MUL2]  Theorem

      |- ∀x1 x2 y1 y2.
           0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 < x2 ∧ y1 < y2 ⇒ x1 * y1 < x2 * y2

   [REAL_LT_MULTIPLE]  Theorem

      |- ∀n d. 1 < n ⇒ (d < &n * d ⇔ 0 < d)

   [REAL_LT_NEG]  Theorem

      |- ∀x y. -x < -y ⇔ y < x

   [REAL_LT_NEGTOTAL]  Theorem

      |- ∀x. (x = 0) ∨ 0 < x ∨ 0 < -x

   [REAL_LT_NZ]  Theorem

      |- ∀n. &n ≠ 0 ⇔ 0 < &n

   [REAL_LT_RADD]  Theorem

      |- ∀x y z. x + z < y + z ⇔ x < y

   [REAL_LT_RDIV]  Theorem

      |- ∀x y z. 0 < z ⇒ (x / z < y / z ⇔ x < y)

   [REAL_LT_RDIV_0]  Theorem

      |- ∀y z. 0 < z ⇒ (0 < y / z ⇔ 0 < y)

   [REAL_LT_RDIV_EQ]  Theorem

      |- ∀x y z. 0 < z ⇒ (x < y / z ⇔ x * z < y)

   [REAL_LT_REFL]  Theorem

      |- ∀x. ¬(x < x)

   [REAL_LT_RMUL]  Theorem

      |- ∀x y z. 0 < z ⇒ (x * z < y * z ⇔ x < y)

   [REAL_LT_RMUL_0]  Theorem

      |- ∀x y. 0 < y ⇒ (0 < x * y ⇔ 0 < x)

   [REAL_LT_RMUL_IMP]  Theorem

      |- ∀x y z. x < y ∧ 0 < z ⇒ x * z < y * z

   [REAL_LT_SUB_LADD]  Theorem

      |- ∀x y z. x < y − z ⇔ x + z < y

   [REAL_LT_SUB_RADD]  Theorem

      |- ∀x y z. x − y < z ⇔ x < z + y

   [REAL_LT_TOTAL]  Theorem

      |- ∀x y. (x = y) ∨ x < y ∨ y < x

   [REAL_LT_TRANS]  Theorem

      |- ∀x y z. x < y ∧ y < z ⇒ x < z

   [REAL_MAX_ADD]  Theorem

      |- ∀z x y. max (x + z) (y + z) = max x y + z

   [REAL_MAX_ALT]  Theorem

      |- ∀x y. (x ≤ y ⇒ (max x y = y)) ∧ (y ≤ x ⇒ (max x y = x))

   [REAL_MAX_LE]  Theorem

      |- ∀z x y. max x y ≤ z ⇔ x ≤ z ∧ y ≤ z

   [REAL_MAX_MIN]  Theorem

      |- ∀x y. max x y = -min (-x) (-y)

   [REAL_MAX_REFL]  Theorem

      |- ∀x. max x x = x

   [REAL_MAX_SUB]  Theorem

      |- ∀z x y. max (x − z) (y − z) = max x y − z

   [REAL_MEAN]  Theorem

      |- ∀x y. x < y ⇒ ∃z. x < z ∧ z < y

   [REAL_MIDDLE1]  Theorem

      |- ∀a b. a ≤ b ⇒ a ≤ (a + b) / 2

   [REAL_MIDDLE2]  Theorem

      |- ∀a b. a ≤ b ⇒ (a + b) / 2 ≤ b

   [REAL_MIN_ADD]  Theorem

      |- ∀z x y. min (x + z) (y + z) = min x y + z

   [REAL_MIN_ALT]  Theorem

      |- ∀x y. (x ≤ y ⇒ (min x y = x)) ∧ (y ≤ x ⇒ (min x y = y))

   [REAL_MIN_LE]  Theorem

      |- ∀z x y. min x y ≤ z ⇔ x ≤ z ∨ y ≤ z

   [REAL_MIN_LE1]  Theorem

      |- ∀x y. min x y ≤ x

   [REAL_MIN_LE2]  Theorem

      |- ∀x y. min x y ≤ y

   [REAL_MIN_LE_LIN]  Theorem

      |- ∀z x y. 0 ≤ z ∧ z ≤ 1 ⇒ min x y ≤ z * x + (1 − z) * y

   [REAL_MIN_MAX]  Theorem

      |- ∀x y. min x y = -max (-x) (-y)

   [REAL_MIN_REFL]  Theorem

      |- ∀x. min x x = x

   [REAL_MIN_SUB]  Theorem

      |- ∀z x y. min (x − z) (y − z) = min x y − z

   [REAL_MUL]  Theorem

      |- ∀m n. &m * &n = &(m * n)

   [REAL_MUL_ASSOC]  Theorem

      |- ∀x y z. x * (y * z) = x * y * z

   [REAL_MUL_COMM]  Theorem

      |- ∀x y. x * y = y * x

   [REAL_MUL_LID]  Theorem

      |- ∀x. 1 * x = x

   [REAL_MUL_LINV]  Theorem

      |- ∀x. x ≠ 0 ⇒ (inv x * x = 1)

   [REAL_MUL_LNEG]  Theorem

      |- ∀x y. -x * y = -(x * y)

   [REAL_MUL_LZERO]  Theorem

      |- ∀x. 0 * x = 0

   [REAL_MUL_RID]  Theorem

      |- ∀x. x * 1 = x

   [REAL_MUL_RINV]  Theorem

      |- ∀x. x ≠ 0 ⇒ (x * inv x = 1)

   [REAL_MUL_RNEG]  Theorem

      |- ∀x y. x * -y = -(x * y)

   [REAL_MUL_RZERO]  Theorem

      |- ∀x. x * 0 = 0

   [REAL_MUL_SUB1_CANCEL]  Theorem

      |- ∀z x y. y * x + y * (z − x) = y * z

   [REAL_MUL_SUB2_CANCEL]  Theorem

      |- ∀z x y. x * y + (z − x) * y = z * y

   [REAL_MUL_SYM]  Theorem

      |- ∀x y. x * y = y * x

   [REAL_NEGNEG]  Theorem

      |- ∀x. --x = x

   [REAL_NEG_0]  Theorem

      |- -0 = 0

   [REAL_NEG_ADD]  Theorem

      |- ∀x y. -(x + y) = -x + -y

   [REAL_NEG_EQ]  Theorem

      |- ∀x y. (-x = y) ⇔ (x = -y)

   [REAL_NEG_EQ0]  Theorem

      |- ∀x. (-x = 0) ⇔ (x = 0)

   [REAL_NEG_GE0]  Theorem

      |- ∀x. 0 ≤ -x ⇔ x ≤ 0

   [REAL_NEG_GT0]  Theorem

      |- ∀x. 0 < -x ⇔ x < 0

   [REAL_NEG_HALF]  Theorem

      |- ∀x. x − x / 2 = x / 2

   [REAL_NEG_INV]  Theorem

      |- ∀x. x ≠ 0 ⇒ (-inv x = inv (-x))

   [REAL_NEG_LE0]  Theorem

      |- ∀x. -x ≤ 0 ⇔ 0 ≤ x

   [REAL_NEG_LMUL]  Theorem

      |- ∀x y. -(x * y) = -x * y

   [REAL_NEG_LT0]  Theorem

      |- ∀x. -x < 0 ⇔ 0 < x

   [REAL_NEG_MINUS1]  Theorem

      |- ∀x. -x = -1 * x

   [REAL_NEG_MUL2]  Theorem

      |- ∀x y. -x * -y = x * y

   [REAL_NEG_NEG]  Theorem

      |- ∀x. --x = x

   [REAL_NEG_RMUL]  Theorem

      |- ∀x y. -(x * y) = x * -y

   [REAL_NEG_SUB]  Theorem

      |- ∀x y. -(x − y) = y − x

   [REAL_NEG_THIRD]  Theorem

      |- ∀x. x − x / 3 = 2 * x / 3

   [REAL_NOT_LE]  Theorem

      |- ∀x y. ¬(x ≤ y) ⇔ y < x

   [REAL_NOT_LT]  Theorem

      |- ∀x y. ¬(x < y) ⇔ y ≤ x

   [REAL_NZ_IMP_LT]  Theorem

      |- ∀n. n ≠ 0 ⇒ 0 < &n

   [REAL_OF_NUM_ADD]  Theorem

      |- ∀m n. &m + &n = &(m + n)

   [REAL_OF_NUM_EQ]  Theorem

      |- ∀m n. (&m = &n) ⇔ (m = n)

   [REAL_OF_NUM_LE]  Theorem

      |- ∀m n. &m ≤ &n ⇔ m ≤ n

   [REAL_OF_NUM_MUL]  Theorem

      |- ∀m n. &m * &n = &(m * n)

   [REAL_OF_NUM_POW]  Theorem

      |- ∀x n. &x pow n = &(x ** n)

   [REAL_OF_NUM_SUC]  Theorem

      |- ∀n. &n + 1 = &SUC n

   [REAL_OVER1]  Theorem

      |- ∀x. x / 1 = x

   [REAL_POASQ]  Theorem

      |- ∀x. 0 < x * x ⇔ x ≠ 0

   [REAL_POS]  Theorem

      |- ∀n. 0 ≤ &n

   [REAL_POS_EQ_ZERO]  Theorem

      |- ∀x. (pos x = 0) ⇔ x ≤ 0

   [REAL_POS_ID]  Theorem

      |- ∀x. 0 ≤ x ⇒ (pos x = x)

   [REAL_POS_INFLATE]  Theorem

      |- ∀x. x ≤ pos x

   [REAL_POS_LE_ZERO]  Theorem

      |- ∀x. pos x ≤ 0 ⇔ x ≤ 0

   [REAL_POS_MONO]  Theorem

      |- ∀x y. x ≤ y ⇒ pos x ≤ pos y

   [REAL_POS_NZ]  Theorem

      |- ∀x. 0 < x ⇒ x ≠ 0

   [REAL_POS_POS]  Theorem

      |- ∀x. 0 ≤ pos x

   [REAL_POW2_ABS]  Theorem

      |- ∀x. abs x pow 2 = x pow 2

   [REAL_POW_ADD]  Theorem

      |- ∀x m n. x pow (m + n) = x pow m * x pow n

   [REAL_POW_DIV]  Theorem

      |- ∀x y n. (x / y) pow n = x pow n / y pow n

   [REAL_POW_INV]  Theorem

      |- ∀x n. inv x pow n = inv (x pow n)

   [REAL_POW_LT]  Theorem

      |- ∀x n. 0 < x ⇒ 0 < x pow n

   [REAL_POW_LT2]  Theorem

      |- ∀n x y. n ≠ 0 ∧ 0 ≤ x ∧ x < y ⇒ x pow n < y pow n

   [REAL_POW_MONO_LT]  Theorem

      |- ∀m n x. 1 < x ∧ m < n ⇒ x pow m < x pow n

   [REAL_POW_POW]  Theorem

      |- ∀x m n. (x pow m) pow n = x pow (m * n)

   [REAL_RDISTRIB]  Theorem

      |- ∀x y z. (x + y) * z = x * z + y * z

   [REAL_RINV_UNIQ]  Theorem

      |- ∀x y. (x * y = 1) ⇒ (y = inv x)

   [REAL_RNEG_UNIQ]  Theorem

      |- ∀x y. (x + y = 0) ⇔ (y = -x)

   [REAL_SUB]  Theorem

      |- ∀m n. &m − &n = if m − n = 0 then -&(n − m) else &(m − n)

   [REAL_SUB_0]  Theorem

      |- ∀x y. (x − y = 0) ⇔ (x = y)

   [REAL_SUB_ABS]  Theorem

      |- ∀x y. abs x − abs y ≤ abs (x − y)

   [REAL_SUB_ADD]  Theorem

      |- ∀x y. x − y + y = x

   [REAL_SUB_ADD2]  Theorem

      |- ∀x y. y + (x − y) = x

   [REAL_SUB_INV2]  Theorem

      |- ∀x y. x ≠ 0 ∧ y ≠ 0 ⇒ (inv x − inv y = (y − x) / (x * y))

   [REAL_SUB_LDISTRIB]  Theorem

      |- ∀x y z. x * (y − z) = x * y − x * z

   [REAL_SUB_LE]  Theorem

      |- ∀x y. 0 ≤ x − y ⇔ y ≤ x

   [REAL_SUB_LNEG]  Theorem

      |- ∀x y. -x − y = -(x + y)

   [REAL_SUB_LT]  Theorem

      |- ∀x y. 0 < x − y ⇔ y < x

   [REAL_SUB_LZERO]  Theorem

      |- ∀x. 0 − x = -x

   [REAL_SUB_NEG2]  Theorem

      |- ∀x y. -x − -y = y − x

   [REAL_SUB_RAT]  Theorem

      |- ∀a b c d.
           b ≠ 0 ∧ d ≠ 0 ⇒ (a / b − c / d = (a * d − b * c) / (b * d))

   [REAL_SUB_RDISTRIB]  Theorem

      |- ∀x y z. (x − y) * z = x * z − y * z

   [REAL_SUB_REFL]  Theorem

      |- ∀x. x − x = 0

   [REAL_SUB_RNEG]  Theorem

      |- ∀x y. x − -y = x + y

   [REAL_SUB_RZERO]  Theorem

      |- ∀x. x − 0 = x

   [REAL_SUB_SUB]  Theorem

      |- ∀x y. x − y − x = -y

   [REAL_SUB_SUB2]  Theorem

      |- ∀x y. x − (x − y) = y

   [REAL_SUB_TRIANGLE]  Theorem

      |- ∀a b c. a − b + (b − c) = a − c

   [REAL_SUMSQ]  Theorem

      |- ∀x y. (x * x + y * y = 0) ⇔ (x = 0) ∧ (y = 0)

   [REAL_SUP]  Theorem

      |- ∀P.
           (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
           ∀y. (∃x. P x ∧ y < x) ⇔ y < sup P

   [REAL_SUP_ALLPOS]  Theorem

      |- ∀P.
           (∀x. P x ⇒ 0 < x) ∧ (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
           ∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s

   [REAL_SUP_CONST]  Theorem

      |- ∀x. sup (λr. r = x) = x

   [REAL_SUP_EXISTS]  Theorem

      |- ∀P.
           (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
           ∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s

   [REAL_SUP_EXISTS_UNIQUE]  Theorem

      |- ∀p.
           (∃x. p x) ∧ (∃z. ∀x. p x ⇒ x ≤ z) ⇒
           ∃!s. ∀y. (∃x. p x ∧ y < x) ⇔ y < s

   [REAL_SUP_LE]  Theorem

      |- ∀P.
           (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇒
           ∀y. (∃x. P x ∧ y < x) ⇔ y < sup P

   [REAL_SUP_MAX]  Theorem

      |- ∀p z. p z ∧ (∀x. p x ⇒ x ≤ z) ⇒ (sup p = z)

   [REAL_SUP_SOMEPOS]  Theorem

      |- ∀P.
           (∃x. P x ∧ 0 < x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒
           ∃s. ∀y. (∃x. P x ∧ y < x) ⇔ y < s

   [REAL_SUP_UBOUND]  Theorem

      |- ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x < z) ⇒ ∀y. P y ⇒ y ≤ sup P

   [REAL_SUP_UBOUND_LE]  Theorem

      |- ∀P. (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇒ ∀y. P y ⇒ y ≤ sup P

   [REAL_THIRDS_BETWEEN]  Theorem

      |- (0 < 1 / 3 ∧ 1 / 3 < 1 ∧ 0 < 2 / 3 ∧ 2 / 3 < 1) ∧ 0 ≤ 1 / 3 ∧
         1 / 3 ≤ 1 ∧ 0 ≤ 2 / 3 ∧ 2 / 3 ≤ 1

   [SETOK_LE_LT]  Theorem

      |- ∀P.
           (∃x. P x) ∧ (∃z. ∀x. P x ⇒ x ≤ z) ⇔
           (∃x. P x) ∧ ∃z. ∀x. P x ⇒ x < z

   [SUM_0]  Theorem

      |- ∀m n. sum (m,n) (λr. 0) = 0

   [SUM_1]  Theorem

      |- ∀f n. sum (n,1) f = f n

   [SUM_2]  Theorem

      |- ∀f n. sum (n,2) f = f n + f (n + 1)

   [SUM_ABS]  Theorem

      |- ∀f m n.
           abs (sum (m,n) (λm. abs (f m))) = sum (m,n) (λm. abs (f m))

   [SUM_ABS_LE]  Theorem

      |- ∀f m n. abs (sum (m,n) f) ≤ sum (m,n) (λn. abs (f n))

   [SUM_ADD]  Theorem

      |- ∀f g m n. sum (m,n) (λn. f n + g n) = sum (m,n) f + sum (m,n) g

   [SUM_BOUND]  Theorem

      |- ∀f k m n. (∀p. m ≤ p ∧ p < m + n ⇒ f p ≤ k) ⇒ sum (m,n) f ≤ &n * k

   [SUM_CANCEL]  Theorem

      |- ∀f n d. sum (n,d) (λn. f (SUC n) − f n) = f (n + d) − f n

   [SUM_CMUL]  Theorem

      |- ∀f c m n. sum (m,n) (λn. c * f n) = c * sum (m,n) f

   [SUM_DIFF]  Theorem

      |- ∀f m n. sum (m,n) f = sum (0,m + n) f − sum (0,m) f

   [SUM_EQ]  Theorem

      |- ∀f g m n.
           (∀r. m ≤ r ∧ r < n + m ⇒ (f r = g r)) ⇒
           (sum (m,n) f = sum (m,n) g)

   [SUM_GROUP]  Theorem

      |- ∀n k f. sum (0,n) (λm. sum (m * k,k) f) = sum (0,n * k) f

   [SUM_LE]  Theorem

      |- ∀f g m n.
           (∀r. m ≤ r ∧ r < n + m ⇒ f r ≤ g r) ⇒ sum (m,n) f ≤ sum (m,n) g

   [SUM_NEG]  Theorem

      |- ∀f n d. sum (n,d) (λn. -f n) = -sum (n,d) f

   [SUM_NSUB]  Theorem

      |- ∀n f c. sum (0,n) f − &n * c = sum (0,n) (λp. f p − c)

   [SUM_OFFSET]  Theorem

      |- ∀f n k. sum (0,n) (λm. f (m + k)) = sum (0,n + k) f − sum (0,k) f

   [SUM_PERMUTE_0]  Theorem

      |- ∀n p.
           (∀y. y < n ⇒ ∃!x. x < n ∧ (p x = y)) ⇒
           ∀f. sum (0,n) (λn. f (p n)) = sum (0,n) f

   [SUM_POS]  Theorem

      |- ∀f. (∀n. 0 ≤ f n) ⇒ ∀m n. 0 ≤ sum (m,n) f

   [SUM_POS_GEN]  Theorem

      |- ∀f m. (∀n. m ≤ n ⇒ 0 ≤ f n) ⇒ ∀n. 0 ≤ sum (m,n) f

   [SUM_REINDEX]  Theorem

      |- ∀f m k n. sum (m + k,n) f = sum (m,n) (λr. f (r + k))

   [SUM_SUB]  Theorem

      |- ∀f g m n. sum (m,n) (λn. f n − g n) = sum (m,n) f − sum (m,n) g

   [SUM_SUBST]  Theorem

      |- ∀f g m n.
           (∀p. m ≤ p ∧ p < m + n ⇒ (f p = g p)) ⇒
           (sum (m,n) f = sum (m,n) g)

   [SUM_TWO]  Theorem

      |- ∀f n p. sum (0,n) f + sum (n,p) f = sum (0,n + p) f

   [SUM_ZERO]  Theorem

      |- ∀f N. (∀n. n ≥ N ⇒ (f n = 0)) ⇒ ∀m n. m ≥ N ⇒ (sum (m,n) f = 0)

   [SUP_EPSILON]  Theorem

      |- ∀p e.
           0 < e ∧ (∃x. p x) ∧ (∃z. ∀x. p x ⇒ x ≤ z) ⇒
           ∃x. p x ∧ sup p ≤ x + e

   [SUP_LEMMA1]  Theorem

      |- ∀P s d.
           (∀y. (∃x. (λx. P (x + d)) x ∧ y < x) ⇔ y < s) ⇒
           ∀y. (∃x. P x ∧ y < x) ⇔ y < s + d

   [SUP_LEMMA2]  Theorem

      |- ∀P. (∃x. P x) ⇒ ∃d x. (λx. P (x + d)) x ∧ 0 < x

   [SUP_LEMMA3]  Theorem

      |- ∀d. (∃z. ∀x. P x ⇒ x < z) ⇒ ∃z. ∀x. (λx. P (x + d)) x ⇒ x < z

   [add_ints]  Theorem

      |- (&n + &m = &(n + m)) ∧
         (-&n + &m = if n ≤ m then &(m − n) else -&(n − m)) ∧
         (&n + -&m = if n < m then -&(m − n) else &(n − m)) ∧
         (-&n + -&m = -&(n + m))

   [add_rat]  Theorem

      |- x / y + u / v =
         if y = 0 then unint (x / y) + u / v
         else if v = 0 then x / y + unint (u / v)
         else if y = v then (x + u) / v
         else (x * v + u * y) / (y * v)

   [add_ratl]  Theorem

      |- x / y + z = if y = 0 then unint (x / y) + z else (x + z * y) / y

   [add_ratr]  Theorem

      |- x + y / z = if z = 0 then x + unint (y / z) else (x * z + y) / z

   [div_rat]  Theorem

      |- x / y / (u / v) =
         if (u = 0) ∨ (v = 0) then x / y / unint (u / v)
         else if y = 0 then unint (x / y) / (u / v)
         else x * v / (y * u)

   [div_ratl]  Theorem

      |- x / y / z =
         if y = 0 then unint (x / y) / z
         else if z = 0 then unint (x / y / z)
         else x / (y * z)

   [div_ratr]  Theorem

      |- x / (y / z) =
         if (y = 0) ∨ (z = 0) then x / unint (y / z) else x * z / y

   [eq_ints]  Theorem

      |- ((&n = &m) ⇔ (n = m)) ∧ ((-&n = &m) ⇔ (n = 0) ∧ (m = 0)) ∧
         ((&n = -&m) ⇔ (n = 0) ∧ (m = 0)) ∧ ((-&n = -&m) ⇔ (n = m))

   [eq_rat]  Theorem

      |- (x / y = u / v) ⇔
         if y = 0 then unint (x / y) = u / v
         else if v = 0 then x / y = unint (u / v)
         else if y = v then x = u
         else x * v = y * u

   [eq_ratl]  Theorem

      |- (x / y = z) ⇔ if y = 0 then unint (x / y) = z else x = y * z

   [eq_ratr]  Theorem

      |- (z = x / y) ⇔ if y = 0 then z = unint (x / y) else y * z = x

   [le_int]  Theorem

      |- (&n ≤ &m ⇔ n ≤ m) ∧ (-&n ≤ &m ⇔ T) ∧
         (&n ≤ -&m ⇔ (n = 0) ∧ (m = 0)) ∧ (-&n ≤ -&m ⇔ m ≤ n)

   [le_rat]  Theorem

      |- x / &n ≤ u / &m ⇔
         if n = 0 then unint (x / 0) ≤ u / &m
         else if m = 0 then x / &n ≤ unint (u / 0)
         else &m * x ≤ &n * u

   [le_ratl]  Theorem

      |- x / &n ≤ u ⇔ if n = 0 then unint (x / 0) ≤ u else x ≤ &n * u

   [le_ratr]  Theorem

      |- x ≤ u / &m ⇔ if m = 0 then x ≤ unint (u / 0) else &m * x ≤ u

   [lt_int]  Theorem

      |- (&n < &m ⇔ n < m) ∧ (-&n < &m ⇔ n ≠ 0 ∨ m ≠ 0) ∧ (&n < -&m ⇔ F) ∧
         (-&n < -&m ⇔ m < n)

   [lt_rat]  Theorem

      |- x / &n < u / &m ⇔
         if n = 0 then unint (x / 0) < u / &m
         else if m = 0 then x / &n < unint (u / 0)
         else &m * x < &n * u

   [lt_ratl]  Theorem

      |- x / &n < u ⇔ if n = 0 then unint (x / 0) < u else x < &n * u

   [lt_ratr]  Theorem

      |- x < u / &m ⇔ if m = 0 then x < unint (u / 0) else &m * x < u

   [mult_ints]  Theorem

      |- (&a * &b = &(a * b)) ∧ (-&a * &b = -&(a * b)) ∧
         (&a * -&b = -&(a * b)) ∧ (-&a * -&b = &(a * b))

   [mult_rat]  Theorem

      |- x / y * (u / v) =
         if y = 0 then unint (x / y) * (u / v)
         else if v = 0 then x / y * unint (u / v)
         else x * u / (y * v)

   [mult_ratl]  Theorem

      |- x / y * z = if y = 0 then unint (x / y) * z else x * z / y

   [mult_ratr]  Theorem

      |- x * (y / z) = if z = 0 then x * unint (y / z) else x * y / z

   [neg_rat]  Theorem

      |- (-(x / y) = if y = 0 then -unint (x / y) else -x / y) ∧
         (x / -y = if y = 0 then unint (x / y) else -x / y)

   [pow_rat]  Theorem

      |- (x pow 0 = 1) ∧ (0 pow NUMERAL (BIT1 n) = 0) ∧
         (0 pow NUMERAL (BIT2 n) = 0) ∧
         (&NUMERAL a pow NUMERAL n = &(NUMERAL a ** NUMERAL n)) ∧
         (-&NUMERAL a pow NUMERAL n =
          (if ODD (NUMERAL n) then numeric_negate else (λx. x))
            (&(NUMERAL a ** NUMERAL n))) ∧
         ((x / y) pow n = x pow n / y pow n)

   [real_lt]  Theorem

      |- ∀y x. x < y ⇔ ¬(y ≤ x)

   [sum]  Theorem

      |- (∀n f. sum (n,0) f = 0) ∧
         ∀n m f. sum (n,SUC m) f = sum (n,m) f + f (n + m)

   [sum_compute]  Theorem

      |- (∀n f. sum (n,0) f = 0) ∧
         (∀n m f.
            sum (n,NUMERAL (BIT1 m)) f =
            sum (n,NUMERAL (BIT1 m) − 1) f +
            f (n + (NUMERAL (BIT1 m) − 1))) ∧
         ∀n m f.
           sum (n,NUMERAL (BIT2 m)) f =
           sum (n,NUMERAL (BIT1 m)) f + f (n + NUMERAL (BIT1 m))

   [sum_ind]  Theorem

      |- ∀P.
           (∀n f. P (n,0) f) ∧ (∀n m f. P (n,m) f ⇒ P (n,SUC m) f) ⇒
           ∀v v1 v2. P (v,v1) v2


*)
end


Source File Identifier index Theory binding index

HOL 4, Kananaskis-10