Structure integerTheory


Source File Identifier index Theory binding index

signature integerTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val EDIV_DEF : thm
    val EMOD_DEF : thm
    val INT_ABS : thm
    val INT_DIVIDES : thm
    val INT_MAX : thm
    val INT_MIN : thm
    val LEAST_INT_DEF : thm
    val Num : thm
    val int_0 : thm
    val int_1 : thm
    val int_ABS_def : thm
    val int_REP_def : thm
    val int_TY_DEF : thm
    val int_add : thm
    val int_bijections : thm
    val int_div : thm
    val int_exp : thm
    val int_ge : thm
    val int_gt : thm
    val int_le : thm
    val int_lt : thm
    val int_mod : thm
    val int_mul : thm
    val int_neg : thm
    val int_of_num : thm
    val int_quot : thm
    val int_rem : thm
    val int_sub : thm
    val tint_0 : thm
    val tint_1 : thm
    val tint_add : thm
    val tint_eq : thm
    val tint_lt : thm
    val tint_mul : thm
    val tint_neg : thm
    val tint_of_num : thm
  
  (*  Theorems  *)
    val EQ_ADDL : thm
    val EQ_LADD : thm
    val FORALL_INT_CASES : thm
    val INFINITE_INT_UNIV : thm
    val INT : thm
    val INT_0 : thm
    val INT_1 : thm
    val INT_10 : thm
    val INT_ABS_0LT : thm
    val INT_ABS_ABS : thm
    val INT_ABS_EQ : thm
    val INT_ABS_EQ0 : thm
    val INT_ABS_EQ_ABS : thm
    val INT_ABS_EQ_ID : thm
    val INT_ABS_LE : thm
    val INT_ABS_LE0 : thm
    val INT_ABS_LT : thm
    val INT_ABS_LT0 : thm
    val INT_ABS_MUL : thm
    val INT_ABS_NEG : thm
    val INT_ABS_NUM : thm
    val INT_ABS_POS : thm
    val INT_ABS_QUOT : thm
    val INT_ABS_SUB : thm
    val INT_ABS_TRIANGLE : thm
    val INT_ADD : thm
    val INT_ADD2_SUB2 : thm
    val INT_ADD_ASSOC : thm
    val INT_ADD_CALCULATE : thm
    val INT_ADD_COMM : thm
    val INT_ADD_DIV : thm
    val INT_ADD_LID : thm
    val INT_ADD_LID_UNIQ : thm
    val INT_ADD_LINV : thm
    val INT_ADD_REDUCE : thm
    val INT_ADD_RID : thm
    val INT_ADD_RID_UNIQ : thm
    val INT_ADD_RINV : thm
    val INT_ADD_SUB : thm
    val INT_ADD_SUB2 : thm
    val INT_ADD_SYM : thm
    val INT_DIFFSQ : thm
    val INT_DISCRETE : thm
    val INT_DIV : thm
    val INT_DIVIDES_0 : thm
    val INT_DIVIDES_1 : thm
    val INT_DIVIDES_LADD : thm
    val INT_DIVIDES_LMUL : thm
    val INT_DIVIDES_LSUB : thm
    val INT_DIVIDES_MOD0 : thm
    val INT_DIVIDES_MUL : thm
    val INT_DIVIDES_MUL_BOTH : thm
    val INT_DIVIDES_NEG : thm
    val INT_DIVIDES_RADD : thm
    val INT_DIVIDES_REDUCE : thm
    val INT_DIVIDES_REFL : thm
    val INT_DIVIDES_RMUL : thm
    val INT_DIVIDES_RSUB : thm
    val INT_DIVIDES_TRANS : thm
    val INT_DIVISION : thm
    val INT_DIV_0 : thm
    val INT_DIV_1 : thm
    val INT_DIV_CALCULATE : thm
    val INT_DIV_EDIV : thm
    val INT_DIV_FORALL_P : thm
    val INT_DIV_ID : thm
    val INT_DIV_LMUL : thm
    val INT_DIV_MUL_ID : thm
    val INT_DIV_NEG : thm
    val INT_DIV_P : thm
    val INT_DIV_REDUCE : thm
    val INT_DIV_RMUL : thm
    val INT_DIV_UNIQUE : thm
    val INT_DOUBLE : thm
    val INT_ENTIRE : thm
    val INT_EQ_CALCULATE : thm
    val INT_EQ_IMP_LE : thm
    val INT_EQ_LADD : thm
    val INT_EQ_LMUL : thm
    val INT_EQ_LMUL2 : thm
    val INT_EQ_LMUL_IMP : thm
    val INT_EQ_NEG : thm
    val INT_EQ_RADD : thm
    val INT_EQ_REDUCE : thm
    val INT_EQ_RMUL : thm
    val INT_EQ_RMUL_IMP : thm
    val INT_EQ_SUB_LADD : thm
    val INT_EQ_SUB_RADD : thm
    val INT_EXP : thm
    val INT_EXP_ADD_EXPONENTS : thm
    val INT_EXP_CALCULATE : thm
    val INT_EXP_EQ0 : thm
    val INT_EXP_MOD : thm
    val INT_EXP_MULTIPLY_EXPONENTS : thm
    val INT_EXP_NEG : thm
    val INT_EXP_REDUCE : thm
    val INT_EXP_SUBTRACT_EXPONENTS : thm
    val INT_GE_CALCULATE : thm
    val INT_GE_REDUCE : thm
    val INT_GT_CALCULATE : thm
    val INT_GT_REDUCE : thm
    val INT_INJ : thm
    val INT_LDISTRIB : thm
    val INT_LE : thm
    val INT_LESS_MOD : thm
    val INT_LET_ADD : thm
    val INT_LET_ADD2 : thm
    val INT_LET_ANTISYM : thm
    val INT_LET_TOTAL : thm
    val INT_LET_TRANS : thm
    val INT_LE_01 : thm
    val INT_LE_ADD : thm
    val INT_LE_ADD2 : thm
    val INT_LE_ADDL : thm
    val INT_LE_ADDR : thm
    val INT_LE_ANTISYM : thm
    val INT_LE_CALCULATE : thm
    val INT_LE_DOUBLE : thm
    val INT_LE_LADD : thm
    val INT_LE_LT : thm
    val INT_LE_LT1 : thm
    val INT_LE_MONO : thm
    val INT_LE_MUL : thm
    val INT_LE_NEG : thm
    val INT_LE_NEGL : thm
    val INT_LE_NEGR : thm
    val INT_LE_NEGTOTAL : thm
    val INT_LE_RADD : thm
    val INT_LE_REDUCE : thm
    val INT_LE_REFL : thm
    val INT_LE_SQUARE : thm
    val INT_LE_SUB_LADD : thm
    val INT_LE_SUB_RADD : thm
    val INT_LE_TOTAL : thm
    val INT_LE_TRANS : thm
    val INT_LNEG_UNIQ : thm
    val INT_LT : thm
    val INT_LTE_ADD : thm
    val INT_LTE_ADD2 : thm
    val INT_LTE_ANTSYM : thm
    val INT_LTE_TOTAL : thm
    val INT_LTE_TRANS : thm
    val INT_LT_01 : thm
    val INT_LT_ADD : thm
    val INT_LT_ADD1 : thm
    val INT_LT_ADD2 : thm
    val INT_LT_ADDL : thm
    val INT_LT_ADDNEG : thm
    val INT_LT_ADDNEG2 : thm
    val INT_LT_ADDR : thm
    val INT_LT_ADD_SUB : thm
    val INT_LT_ANTISYM : thm
    val INT_LT_CALCULATE : thm
    val INT_LT_GT : thm
    val INT_LT_IMP_LE : thm
    val INT_LT_IMP_NE : thm
    val INT_LT_LADD : thm
    val INT_LT_LADD_IMP : thm
    val INT_LT_LE : thm
    val INT_LT_LE1 : thm
    val INT_LT_MONO : thm
    val INT_LT_MUL : thm
    val INT_LT_MUL2 : thm
    val INT_LT_NEG : thm
    val INT_LT_NEGTOTAL : thm
    val INT_LT_NZ : thm
    val INT_LT_RADD : thm
    val INT_LT_REDUCE : thm
    val INT_LT_REFL : thm
    val INT_LT_SUB_LADD : thm
    val INT_LT_SUB_RADD : thm
    val INT_LT_TOTAL : thm
    val INT_LT_TRANS : thm
    val INT_MAX_LT : thm
    val INT_MAX_NUM : thm
    val INT_MIN_LT : thm
    val INT_MIN_NUM : thm
    val INT_MOD : thm
    val INT_MOD0 : thm
    val INT_MOD_1 : thm
    val INT_MOD_ADD_MULTIPLES : thm
    val INT_MOD_BOUNDS : thm
    val INT_MOD_CALCULATE : thm
    val INT_MOD_COMMON_FACTOR : thm
    val INT_MOD_EMOD : thm
    val INT_MOD_EQ0 : thm
    val INT_MOD_FORALL_P : thm
    val INT_MOD_ID : thm
    val INT_MOD_MINUS1 : thm
    val INT_MOD_MOD : thm
    val INT_MOD_NEG : thm
    val INT_MOD_NEG_NUMERATOR : thm
    val INT_MOD_P : thm
    val INT_MOD_PLUS : thm
    val INT_MOD_REDUCE : thm
    val INT_MOD_SUB : thm
    val INT_MOD_UNIQUE : thm
    val INT_MUL : thm
    val INT_MUL_ASSOC : thm
    val INT_MUL_CALCULATE : thm
    val INT_MUL_COMM : thm
    val INT_MUL_DIV : thm
    val INT_MUL_EQ_1 : thm
    val INT_MUL_LID : thm
    val INT_MUL_LZERO : thm
    val INT_MUL_QUOT : thm
    val INT_MUL_REDUCE : thm
    val INT_MUL_RID : thm
    val INT_MUL_RZERO : thm
    val INT_MUL_SIGN_CASES : thm
    val INT_MUL_SYM : thm
    val INT_NEGNEG : thm
    val INT_NEG_0 : thm
    val INT_NEG_ADD : thm
    val INT_NEG_EQ : thm
    val INT_NEG_EQ0 : thm
    val INT_NEG_GE0 : thm
    val INT_NEG_GT0 : thm
    val INT_NEG_LE0 : thm
    val INT_NEG_LMUL : thm
    val INT_NEG_LT0 : thm
    val INT_NEG_MINUS1 : thm
    val INT_NEG_MUL2 : thm
    val INT_NEG_RMUL : thm
    val INT_NEG_SAME_EQ : thm
    val INT_NEG_SUB : thm
    val INT_NOT_LE : thm
    val INT_NOT_LT : thm
    val INT_NUM_CASES : thm
    val INT_NZ_IMP_LT : thm
    val INT_OF_NUM : thm
    val INT_POS : thm
    val INT_POSSQ : thm
    val INT_POS_NZ : thm
    val INT_QUOT : thm
    val INT_QUOT_0 : thm
    val INT_QUOT_1 : thm
    val INT_QUOT_CALCULATE : thm
    val INT_QUOT_EDIV : thm
    val INT_QUOT_ID : thm
    val INT_QUOT_NEG : thm
    val INT_QUOT_REDUCE : thm
    val INT_QUOT_UNIQUE : thm
    val INT_RDISTRIB : thm
    val INT_REM : thm
    val INT_REM0 : thm
    val INT_REMQUOT : thm
    val INT_REM_CALCULATE : thm
    val INT_REM_COMMON_FACTOR : thm
    val INT_REM_EMOD : thm
    val INT_REM_EQ0 : thm
    val INT_REM_EQ_MOD : thm
    val INT_REM_ID : thm
    val INT_REM_NEG : thm
    val INT_REM_REDUCE : thm
    val INT_REM_UNIQUE : thm
    val INT_RNEG_UNIQ : thm
    val INT_SUB : thm
    val INT_SUB_0 : thm
    val INT_SUB_ABS_TRIANGLE : thm
    val INT_SUB_ADD : thm
    val INT_SUB_ADD2 : thm
    val INT_SUB_CALCULATE : thm
    val INT_SUB_LDISTRIB : thm
    val INT_SUB_LE : thm
    val INT_SUB_LNEG : thm
    val INT_SUB_LT : thm
    val INT_SUB_LZERO : thm
    val INT_SUB_NEG2 : thm
    val INT_SUB_RDISTRIB : thm
    val INT_SUB_REDUCE : thm
    val INT_SUB_REFL : thm
    val INT_SUB_RNEG : thm
    val INT_SUB_RZERO : thm
    val INT_SUB_SUB : thm
    val INT_SUB_SUB2 : thm
    val INT_SUB_TRIANGLE : thm
    val INT_SUMSQ : thm
    val LE_NUM_OF_INT : thm
    val LT_ADD2 : thm
    val LT_ADDL : thm
    val LT_ADDR : thm
    val LT_LADD : thm
    val NUM_EQ0 : thm
    val NUM_INT_ADD : thm
    val NUM_INT_EDIV : thm
    val NUM_INT_EMOD : thm
    val NUM_INT_MUL : thm
    val NUM_INT_SUB : thm
    val NUM_LT : thm
    val NUM_NEGINT_EXISTS : thm
    val NUM_OF_INT : thm
    val NUM_OF_NEG_INT : thm
    val NUM_POSINT : thm
    val NUM_POSINT_EX : thm
    val NUM_POSINT_EXISTS : thm
    val NUM_POSTINT_EX : thm
    val Num_EQ : thm
    val Num_EQ_ABS : thm
    val Num_neg : thm
    val TINT_10 : thm
    val TINT_ADD_ASSOC : thm
    val TINT_ADD_LID : thm
    val TINT_ADD_LINV : thm
    val TINT_ADD_SYM : thm
    val TINT_ADD_WELLDEF : thm
    val TINT_ADD_WELLDEFR : thm
    val TINT_EQ_AP : thm
    val TINT_EQ_EQUIV : thm
    val TINT_EQ_REFL : thm
    val TINT_EQ_SYM : thm
    val TINT_EQ_TRANS : thm
    val TINT_INJ : thm
    val TINT_LDISTRIB : thm
    val TINT_LT_ADD : thm
    val TINT_LT_MUL : thm
    val TINT_LT_REFL : thm
    val TINT_LT_TOTAL : thm
    val TINT_LT_TRANS : thm
    val TINT_LT_WELLDEF : thm
    val TINT_LT_WELLDEFL : thm
    val TINT_LT_WELLDEFR : thm
    val TINT_MUL_ASSOC : thm
    val TINT_MUL_LID : thm
    val TINT_MUL_SYM : thm
    val TINT_MUL_WELLDEF : thm
    val TINT_MUL_WELLDEFR : thm
    val TINT_NEG_WELLDEF : thm
    val int_ABS_REP_CLASS : thm
    val int_QUOTIENT : thm
    val int_eq_calculate : thm
    val num_of_int : thm
    val tint_of_num_eq : thm
  
  val integer_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [indexedLists] Parent theory of "integer"
   
   [patternMatches] Parent theory of "integer"
   
   [EDIV_DEF]  Definition
      
      ⊢ ∀i j. ediv i j = if 0 < j then i / j else -(i / -j)
   
   [EMOD_DEF]  Definition
      
      ⊢ ∀i j. emod i j = i % ABS j
   
   [INT_ABS]  Definition
      
      ⊢ ∀n. ABS n = if n < 0 then -n else n
   
   [INT_DIVIDES]  Definition
      
      ⊢ ∀p q. p int_divides q ⇔ ∃m. m * p = q
   
   [INT_MAX]  Definition
      
      ⊢ ∀x y. int_max x y = if x < y then y else x
   
   [INT_MIN]  Definition
      
      ⊢ ∀x y. int_min x y = if x < y then x else y
   
   [LEAST_INT_DEF]  Definition
      
      ⊢ ∀P. $LEAST_INT P = @i. P i ∧ ∀j. j < i ⇒ ¬P j
   
   [Num]  Definition
      
      ⊢ ∀i. Num i = @n. if 0 ≤ i then i = &n else i = -&n
   
   [int_0]  Definition
      
      ⊢ int_0 = int_ABS tint_0
   
   [int_1]  Definition
      
      ⊢ int_1 = int_ABS tint_1
   
   [int_ABS_def]  Definition
      
      ⊢ ∀r. int_ABS r = int_ABS_CLASS ($tint_eq r)
   
   [int_REP_def]  Definition
      
      ⊢ ∀a. int_REP a = $@ (int_REP_CLASS a)
   
   [int_TY_DEF]  Definition
      
      ⊢ ∃rep. TYPE_DEFINITION (λc. ∃r. r tint_eq r ∧ c = $tint_eq r) rep
   
   [int_add]  Definition
      
      ⊢ ∀T1 T2. T1 + T2 = int_ABS (int_REP T1 tint_add int_REP T2)
   
   [int_bijections]  Definition
      
      ⊢ (∀a. int_ABS_CLASS (int_REP_CLASS a) = a) ∧
        ∀r. (λc. ∃r. r tint_eq r ∧ c = $tint_eq r) r ⇔
            int_REP_CLASS (int_ABS_CLASS r) = r
   
   [int_div]  Definition
      
      ⊢ ∀i j.
          j ≠ 0 ⇒
          i / j =
          if 0 < j then
            if 0 ≤ i then &(Num i DIV Num j)
            else
              -&(Num (-i) DIV Num j) +
              if Num (-i) MOD Num j = 0 then 0 else -1
          else if 0 ≤ i then
            -&(Num i DIV Num (-j)) +
            if Num i MOD Num (-j) = 0 then 0 else -1
          else &(Num (-i) DIV Num (-j))
   
   [int_exp]  Definition
      
      ⊢ (∀p. p ** 0 = 1) ∧ ∀p n. p ** SUC n = p * p ** n
   
   [int_ge]  Definition
      
      ⊢ ∀x y. x ≥ y ⇔ y ≤ x
   
   [int_gt]  Definition
      
      ⊢ ∀x y. x > y ⇔ y < x
   
   [int_le]  Definition
      
      ⊢ ∀x y. x ≤ y ⇔ ¬(y < x)
   
   [int_lt]  Definition
      
      ⊢ ∀T1 T2. T1 < T2 ⇔ int_REP T1 tint_lt int_REP T2
   
   [int_mod]  Definition
      
      ⊢ ∀i j. j ≠ 0 ⇒ i % j = i − i / j * j
   
   [int_mul]  Definition
      
      ⊢ ∀T1 T2. T1 * T2 = int_ABS (int_REP T1 tint_mul int_REP T2)
   
   [int_neg]  Definition
      
      ⊢ ∀T1. -T1 = int_ABS (tint_neg (int_REP T1))
   
   [int_of_num]  Definition
      
      ⊢ ∀T1. &T1 = int_ABS (tint_of_num T1)
   
   [int_quot]  Definition
      
      ⊢ ∀i j.
          j ≠ 0 ⇒
          i quot j =
          if 0 < j then
            if 0 ≤ i then &(Num i DIV Num j) else -&(Num (-i) DIV Num j)
          else if 0 ≤ i then -&(Num i DIV Num (-j))
          else &(Num (-i) DIV Num (-j))
   
   [int_rem]  Definition
      
      ⊢ ∀i j. j ≠ 0 ⇒ i rem j = i − i quot j * j
   
   [int_sub]  Definition
      
      ⊢ ∀x y. x − y = x + -y
   
   [tint_0]  Definition
      
      ⊢ tint_0 = (1,1)
   
   [tint_1]  Definition
      
      ⊢ tint_1 = (1 + 1,1)
   
   [tint_add]  Definition
      
      ⊢ ∀x1 y1 x2 y2. (x1,y1) tint_add (x2,y2) = (x1 + x2,y1 + y2)
   
   [tint_eq]  Definition
      
      ⊢ ∀x1 y1 x2 y2. (x1,y1) tint_eq (x2,y2) ⇔ x1 + y2 = x2 + y1
   
   [tint_lt]  Definition
      
      ⊢ ∀x1 y1 x2 y2. (x1,y1) tint_lt (x2,y2) ⇔ x1 + y2 < x2 + y1
   
   [tint_mul]  Definition
      
      ⊢ ∀x1 y1 x2 y2.
          (x1,y1) tint_mul (x2,y2) = (x1 * x2 + y1 * y2,x1 * y2 + y1 * x2)
   
   [tint_neg]  Definition
      
      ⊢ ∀x y. tint_neg (x,y) = (y,x)
   
   [tint_of_num]  Definition
      
      ⊢ tint_of_num 0 = tint_0 ∧
        ∀n. tint_of_num (SUC n) = tint_of_num n tint_add tint_1
   
   [EQ_ADDL]  Theorem
      
      ⊢ ∀x y. x = x + y ⇔ y = 0
   
   [EQ_LADD]  Theorem
      
      ⊢ ∀x y z. x + y = x + z ⇔ y = z
   
   [FORALL_INT_CASES]  Theorem
      
      ⊢ ∀P. (∀x. P x) ⇔ (∀n. P (&n)) ∧ ∀n. P (-&n)
   
   [INFINITE_INT_UNIV]  Theorem
      
      ⊢ INFINITE 𝕌(:int)
   
   [INT]  Theorem
      
      ⊢ ∀n. &SUC n = &n + 1
   
   [INT_0]  Theorem
      
      ⊢ int_0 = 0
   
   [INT_1]  Theorem
      
      ⊢ int_1 = 1
   
   [INT_10]  Theorem
      
      ⊢ int_1 ≠ int_0
   
   [INT_ABS_0LT]  Theorem
      
      ⊢ 0 < ABS p ⇔ p ≠ 0
   
   [INT_ABS_ABS]  Theorem
      
      ⊢ ∀p. ABS (ABS p) = ABS p
   
   [INT_ABS_EQ]  Theorem
      
      ⊢ ∀p q.
          (ABS p = q ⇔ p = q ∧ 0 < q ∨ p = -q ∧ 0 ≤ q) ∧
          (q = ABS p ⇔ p = q ∧ 0 < q ∨ p = -q ∧ 0 ≤ q)
   
   [INT_ABS_EQ0]  Theorem
      
      ⊢ ∀p. ABS p = 0 ⇔ p = 0
   
   [INT_ABS_EQ_ABS]  Theorem
      
      ⊢ ABS x = ABS y ⇔ x = y ∨ x = -y
   
   [INT_ABS_EQ_ID]  Theorem
      
      ⊢ ∀p. ABS p = p ⇔ 0 ≤ p
   
   [INT_ABS_LE]  Theorem
      
      ⊢ ∀p q.
          (ABS p ≤ q ⇔ p ≤ q ∧ -q ≤ p) ∧ (q ≤ ABS p ⇔ q ≤ p ∨ p ≤ -q) ∧
          (-ABS p ≤ q ⇔ -q ≤ p ∨ p ≤ q) ∧ (q ≤ -ABS p ⇔ p ≤ -q ∧ q ≤ p)
   
   [INT_ABS_LE0]  Theorem
      
      ⊢ ∀p. ABS p ≤ 0 ⇔ p = 0
   
   [INT_ABS_LT]  Theorem
      
      ⊢ ∀p q.
          (ABS p < q ⇔ p < q ∧ -q < p) ∧ (q < ABS p ⇔ q < p ∨ p < -q) ∧
          (-ABS p < q ⇔ -q < p ∨ p < q) ∧ (q < -ABS p ⇔ p < -q ∧ q < p)
   
   [INT_ABS_LT0]  Theorem
      
      ⊢ ∀p. ¬(ABS p < 0)
   
   [INT_ABS_MUL]  Theorem
      
      ⊢ ∀p q. ABS p * ABS q = ABS (p * q)
   
   [INT_ABS_NEG]  Theorem
      
      ⊢ ∀p. ABS (-p) = ABS p
   
   [INT_ABS_NUM]  Theorem
      
      ⊢ ∀n. ABS (&n) = &n
   
   [INT_ABS_POS]  Theorem
      
      ⊢ ∀p. 0 ≤ ABS p
   
   [INT_ABS_QUOT]  Theorem
      
      ⊢ ∀p q. q ≠ 0 ⇒ ABS (p quot q * q) ≤ ABS p
   
   [INT_ABS_SUB]  Theorem
      
      ⊢ ABS (i − j) = ABS (j − i)
   
   [INT_ABS_TRIANGLE]  Theorem
      
      ⊢ ABS (i + j) ≤ ABS i + ABS j
   
   [INT_ADD]  Theorem
      
      ⊢ ∀m n. &m + &n = &(m + n)
   
   [INT_ADD2_SUB2]  Theorem
      
      ⊢ ∀a b c d. a + b − (c + d) = a − c + (b − d)
   
   [INT_ADD_ASSOC]  Theorem
      
      ⊢ ∀z y x. x + (y + z) = x + y + z
   
   [INT_ADD_CALCULATE]  Theorem
      
      ⊢ ∀p n m.
          0 + p = p ∧ p + 0 = p ∧ &n + &m = &(n + m) ∧
          &n + -&m = (if m ≤ n then &(n − m) else -&(m − n)) ∧
          -&n + &m = (if n ≤ m then &(m − n) else -&(n − m)) ∧
          -&n + -&m = -&(n + m)
   
   [INT_ADD_COMM]  Theorem
      
      ⊢ ∀y x. x + y = y + x
   
   [INT_ADD_DIV]  Theorem
      
      ⊢ ∀i j k.
          k ≠ 0 ∧ (i % k = 0 ∨ j % k = 0) ⇒ (i + j) / k = i / k + j / k
   
   [INT_ADD_LID]  Theorem
      
      ⊢ ∀x. 0 + x = x
   
   [INT_ADD_LID_UNIQ]  Theorem
      
      ⊢ ∀x y. x + y = y ⇔ x = 0
   
   [INT_ADD_LINV]  Theorem
      
      ⊢ ∀x. -x + x = 0
   
   [INT_ADD_REDUCE]  Theorem
      
      ⊢ ∀p n m.
          0 + p = p ∧ p + 0 = p ∧ -0 = 0 ∧ --p = p ∧
          &NUMERAL n + &NUMERAL m = &NUMERAL (numeral$iZ (n + m)) ∧
          &NUMERAL n + -&NUMERAL m =
          (if m ≤ n then &NUMERAL (n − m) else -&NUMERAL (m − n)) ∧
          -&NUMERAL n + &NUMERAL m =
          (if n ≤ m then &NUMERAL (m − n) else -&NUMERAL (n − m)) ∧
          -&NUMERAL n + -&NUMERAL m = -&NUMERAL (numeral$iZ (n + m))
   
   [INT_ADD_RID]  Theorem
      
      ⊢ ∀x. x + 0 = x
   
   [INT_ADD_RID_UNIQ]  Theorem
      
      ⊢ ∀x y. x + y = x ⇔ y = 0
   
   [INT_ADD_RINV]  Theorem
      
      ⊢ ∀x. x + -x = 0
   
   [INT_ADD_SUB]  Theorem
      
      ⊢ ∀x y. x + y − x = y
   
   [INT_ADD_SUB2]  Theorem
      
      ⊢ ∀x y. x − (x + y) = -y
   
   [INT_ADD_SYM]  Theorem
      
      ⊢ ∀y x. x + y = y + x
   
   [INT_DIFFSQ]  Theorem
      
      ⊢ ∀x y. (x + y) * (x − y) = x * x − y * y
   
   [INT_DISCRETE]  Theorem
      
      ⊢ ∀x y. ¬(x < y ∧ y < x + 1)
   
   [INT_DIV]  Theorem
      
      ⊢ ∀n m. m ≠ 0 ⇒ &n / &m = &(n DIV m)
   
   [INT_DIVIDES_0]  Theorem
      
      ⊢ (∀x. x int_divides 0) ∧ ∀x. 0 int_divides x ⇔ x = 0
   
   [INT_DIVIDES_1]  Theorem
      
      ⊢ ∀x. 1 int_divides x ∧ (x int_divides 1 ⇔ x = 1 ∨ x = -1)
   
   [INT_DIVIDES_LADD]  Theorem
      
      ⊢ ∀p q r. p int_divides q ⇒ (p int_divides q + r ⇔ p int_divides r)
   
   [INT_DIVIDES_LMUL]  Theorem
      
      ⊢ ∀p q r. p int_divides q ⇒ p int_divides q * r
   
   [INT_DIVIDES_LSUB]  Theorem
      
      ⊢ ∀p q r. p int_divides q ⇒ (p int_divides q − r ⇔ p int_divides r)
   
   [INT_DIVIDES_MOD0]  Theorem
      
      ⊢ ∀p q. p int_divides q ⇔ q % p = 0 ∧ p ≠ 0 ∨ p = 0 ∧ q = 0
   
   [INT_DIVIDES_MUL]  Theorem
      
      ⊢ ∀p q. p int_divides p * q ∧ p int_divides q * p
   
   [INT_DIVIDES_MUL_BOTH]  Theorem
      
      ⊢ ∀p q r. p ≠ 0 ⇒ (p * q int_divides p * r ⇔ q int_divides r)
   
   [INT_DIVIDES_NEG]  Theorem
      
      ⊢ ∀p q.
          (p int_divides -q ⇔ p int_divides q) ∧
          (-p int_divides q ⇔ p int_divides q)
   
   [INT_DIVIDES_RADD]  Theorem
      
      ⊢ ∀p q r. p int_divides q ⇒ (p int_divides r + q ⇔ p int_divides r)
   
   [INT_DIVIDES_REDUCE]  Theorem
      
      ⊢ ∀n m p.
          (0 int_divides 0 ⇔ T) ∧ (0 int_divides &NUMERAL (BIT1 n) ⇔ F) ∧
          (0 int_divides &NUMERAL (BIT2 n) ⇔ F) ∧ (p int_divides 0 ⇔ T) ∧
          (&NUMERAL (BIT1 n) int_divides &NUMERAL m ⇔
           NUMERAL m MOD NUMERAL (BIT1 n) = 0) ∧
          (&NUMERAL (BIT2 n) int_divides &NUMERAL m ⇔
           NUMERAL m MOD NUMERAL (BIT2 n) = 0) ∧
          (&NUMERAL (BIT1 n) int_divides -&NUMERAL m ⇔
           NUMERAL m MOD NUMERAL (BIT1 n) = 0) ∧
          (&NUMERAL (BIT2 n) int_divides -&NUMERAL m ⇔
           NUMERAL m MOD NUMERAL (BIT2 n) = 0) ∧
          (-&NUMERAL (BIT1 n) int_divides &NUMERAL m ⇔
           NUMERAL m MOD NUMERAL (BIT1 n) = 0) ∧
          (-&NUMERAL (BIT2 n) int_divides &NUMERAL m ⇔
           NUMERAL m MOD NUMERAL (BIT2 n) = 0) ∧
          (-&NUMERAL (BIT1 n) int_divides -&NUMERAL m ⇔
           NUMERAL m MOD NUMERAL (BIT1 n) = 0) ∧
          (-&NUMERAL (BIT2 n) int_divides -&NUMERAL m ⇔
           NUMERAL m MOD NUMERAL (BIT2 n) = 0)
   
   [INT_DIVIDES_REFL]  Theorem
      
      ⊢ ∀x. x int_divides x
   
   [INT_DIVIDES_RMUL]  Theorem
      
      ⊢ ∀p q r. p int_divides q ⇒ p int_divides r * q
   
   [INT_DIVIDES_RSUB]  Theorem
      
      ⊢ ∀p q r. p int_divides q ⇒ (p int_divides r − q ⇔ p int_divides r)
   
   [INT_DIVIDES_TRANS]  Theorem
      
      ⊢ ∀x y z. x int_divides y ∧ y int_divides z ⇒ x int_divides z
   
   [INT_DIVISION]  Theorem
      
      ⊢ ∀q. q ≠ 0 ⇒
            ∀p. p = p / q * q + p % q ∧
                if q < 0 then q < p % q ∧ p % q ≤ 0
                else 0 ≤ p % q ∧ p % q < q
   
   [INT_DIV_0]  Theorem
      
      ⊢ ∀q. q ≠ 0 ⇒ 0 / q = 0
   
   [INT_DIV_1]  Theorem
      
      ⊢ ∀p. p / 1 = p
   
   [INT_DIV_CALCULATE]  Theorem
      
      ⊢ (∀n m. m ≠ 0 ⇒ &n / &m = &(n DIV m)) ∧
        (∀p q. q ≠ 0 ⇒ p / -q = -p / q) ∧ (∀m n. &m = &n ⇔ m = n) ∧
        (∀x. -x = 0 ⇔ x = 0) ∧ ∀x. --x = x
   
   [INT_DIV_EDIV]  Theorem
      
      ⊢ ∀i j. j ≠ 0 ⇒ i / j = if 0 < j then ediv i j else -ediv (-i) j
   
   [INT_DIV_FORALL_P]  Theorem
      
      ⊢ ∀P x c.
          c ≠ 0 ⇒
          (P (x / c) ⇔
           ∀k r.
             x = k * c + r ∧
             (c < 0 ∧ c < r ∧ r ≤ 0 ∨ ¬(c < 0) ∧ 0 ≤ r ∧ r < c) ⇒
             P k)
   
   [INT_DIV_ID]  Theorem
      
      ⊢ ∀p. p ≠ 0 ⇒ p / p = 1
   
   [INT_DIV_LMUL]  Theorem
      
      ⊢ ∀i j. i ≠ 0 ⇒ i * j / i = j
   
   [INT_DIV_MUL_ID]  Theorem
      
      ⊢ ∀p q. q ≠ 0 ∧ p % q = 0 ⇒ p / q * q = p
   
   [INT_DIV_NEG]  Theorem
      
      ⊢ ∀p q. q ≠ 0 ⇒ p / -q = -p / q
   
   [INT_DIV_P]  Theorem
      
      ⊢ ∀P x c.
          c ≠ 0 ⇒
          (P (x / c) ⇔
           ∃k r.
             x = k * c + r ∧
             (c < 0 ∧ c < r ∧ r ≤ 0 ∨ ¬(c < 0) ∧ 0 ≤ r ∧ r < c) ∧ P k)
   
   [INT_DIV_REDUCE]  Theorem
      
      ⊢ ∀m n.
          0 / &NUMERAL (BIT1 n) = 0 ∧ 0 / &NUMERAL (BIT2 n) = 0 ∧
          &NUMERAL m / &NUMERAL (BIT1 n) =
          &(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
          &NUMERAL m / &NUMERAL (BIT2 n) =
          &(NUMERAL m DIV NUMERAL (BIT2 n)) ∧
          -&NUMERAL m / &NUMERAL (BIT1 n) =
          -&(NUMERAL m DIV NUMERAL (BIT1 n)) +
          (if NUMERAL m MOD NUMERAL (BIT1 n) = 0 then 0 else -1) ∧
          -&NUMERAL m / &NUMERAL (BIT2 n) =
          -&(NUMERAL m DIV NUMERAL (BIT2 n)) +
          (if NUMERAL m MOD NUMERAL (BIT2 n) = 0 then 0 else -1) ∧
          &NUMERAL m / -&NUMERAL (BIT1 n) =
          -&(NUMERAL m DIV NUMERAL (BIT1 n)) +
          (if NUMERAL m MOD NUMERAL (BIT1 n) = 0 then 0 else -1) ∧
          &NUMERAL m / -&NUMERAL (BIT2 n) =
          -&(NUMERAL m DIV NUMERAL (BIT2 n)) +
          (if NUMERAL m MOD NUMERAL (BIT2 n) = 0 then 0 else -1) ∧
          -&NUMERAL m / -&NUMERAL (BIT1 n) =
          &(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
          -&NUMERAL m / -&NUMERAL (BIT2 n) =
          &(NUMERAL m DIV NUMERAL (BIT2 n))
   
   [INT_DIV_RMUL]  Theorem
      
      ⊢ ∀i j. i ≠ 0 ⇒ j * i / i = j
   
   [INT_DIV_UNIQUE]  Theorem
      
      ⊢ ∀i j q.
          (∃r. i = q * j + r ∧
               if j < 0 then j < r ∧ r ≤ 0 else 0 ≤ r ∧ r < j) ⇒
          i / j = q
   
   [INT_DOUBLE]  Theorem
      
      ⊢ ∀x. x + x = 2 * x
   
   [INT_ENTIRE]  Theorem
      
      ⊢ ∀x y. x * y = 0 ⇔ x = 0 ∨ y = 0
   
   [INT_EQ_CALCULATE]  Theorem
      
      ⊢ (∀m n. &m = &n ⇔ m = n) ∧ (∀x y. -x = -y ⇔ x = y) ∧
        ∀n m. (&n = -&m ⇔ n = 0 ∧ m = 0) ∧ (-&n = &m ⇔ n = 0 ∧ m = 0)
   
   [INT_EQ_IMP_LE]  Theorem
      
      ⊢ ∀x y. x = y ⇒ x ≤ y
   
   [INT_EQ_LADD]  Theorem
      
      ⊢ ∀x y z. x + y = x + z ⇔ y = z
   
   [INT_EQ_LMUL]  Theorem
      
      ⊢ ∀x y z. x * y = x * z ⇔ x = 0 ∨ y = z
   
   [INT_EQ_LMUL2]  Theorem
      
      ⊢ ∀x y z. x ≠ 0 ⇒ (y = z ⇔ x * y = x * z)
   
   [INT_EQ_LMUL_IMP]  Theorem
      
      ⊢ ∀x y z. x ≠ 0 ∧ x * y = x * z ⇒ y = z
   
   [INT_EQ_NEG]  Theorem
      
      ⊢ ∀x y. -x = -y ⇔ x = y
   
   [INT_EQ_RADD]  Theorem
      
      ⊢ ∀x y z. x + z = y + z ⇔ x = y
   
   [INT_EQ_REDUCE]  Theorem
      
      ⊢ ∀n m.
          (0 = 0 ⇔ T) ∧ (0 = &NUMERAL (BIT1 n) ⇔ F) ∧
          (0 = &NUMERAL (BIT2 n) ⇔ F) ∧ (0 = -&NUMERAL (BIT1 n) ⇔ F) ∧
          (0 = -&NUMERAL (BIT2 n) ⇔ F) ∧ (&NUMERAL (BIT1 n) = 0 ⇔ F) ∧
          (&NUMERAL (BIT2 n) = 0 ⇔ F) ∧ (-&NUMERAL (BIT1 n) = 0 ⇔ F) ∧
          (-&NUMERAL (BIT2 n) = 0 ⇔ F) ∧
          (&NUMERAL n = &NUMERAL m ⇔ n = m) ∧
          (&NUMERAL (BIT1 n) = -&NUMERAL m ⇔ F) ∧
          (&NUMERAL (BIT2 n) = -&NUMERAL m ⇔ F) ∧
          (-&NUMERAL (BIT1 n) = &NUMERAL m ⇔ F) ∧
          (-&NUMERAL (BIT2 n) = &NUMERAL m ⇔ F) ∧
          (-&NUMERAL n = -&NUMERAL m ⇔ n = m)
   
   [INT_EQ_RMUL]  Theorem
      
      ⊢ ∀x y z. x * z = y * z ⇔ z = 0 ∨ x = y
   
   [INT_EQ_RMUL_IMP]  Theorem
      
      ⊢ ∀x y z. z ≠ 0 ∧ x * z = y * z ⇒ x = y
   
   [INT_EQ_SUB_LADD]  Theorem
      
      ⊢ ∀x y z. x = y − z ⇔ x + z = y
   
   [INT_EQ_SUB_RADD]  Theorem
      
      ⊢ ∀x y z. x − y = z ⇔ x = z + y
   
   [INT_EXP]  Theorem
      
      ⊢ ∀n m. &n ** m = &(n ** m)
   
   [INT_EXP_ADD_EXPONENTS]  Theorem
      
      ⊢ ∀n m p. p ** n * p ** m = p ** (n + m)
   
   [INT_EXP_CALCULATE]  Theorem
      
      ⊢ ∀p n m.
          p ** 0 = 1 ∧ &n ** m = &(n ** m) ∧
          -&n ** NUMERAL (BIT1 m) = -&NUMERAL (n ** NUMERAL (BIT1 m)) ∧
          -&n ** NUMERAL (BIT2 m) = &NUMERAL (n ** NUMERAL (BIT2 m))
   
   [INT_EXP_EQ0]  Theorem
      
      ⊢ ∀p n. p ** n = 0 ⇔ p = 0 ∧ n ≠ 0
   
   [INT_EXP_MOD]  Theorem
      
      ⊢ ∀m n p. n ≤ m ∧ p ≠ 0 ⇒ p ** m % p ** n = 0
   
   [INT_EXP_MULTIPLY_EXPONENTS]  Theorem
      
      ⊢ ∀m n p. (p ** n) ** m = p ** (n * m)
   
   [INT_EXP_NEG]  Theorem
      
      ⊢ ∀n m.
          (EVEN n ⇒ -&m ** n = &(m ** n)) ∧ (ODD n ⇒ -&m ** n = -&(m ** n))
   
   [INT_EXP_REDUCE]  Theorem
      
      ⊢ ∀n m p.
          p ** 0 = 1 ∧ &NUMERAL n ** NUMERAL m = &NUMERAL (n ** m) ∧
          -&NUMERAL n ** NUMERAL (BIT1 m) = -&NUMERAL (n ** BIT1 m) ∧
          -&NUMERAL n ** NUMERAL (BIT2 m) = &NUMERAL (n ** BIT2 m)
   
   [INT_EXP_SUBTRACT_EXPONENTS]  Theorem
      
      ⊢ ∀m n p. n ≤ m ∧ p ≠ 0 ⇒ p ** m / p ** n = p ** (m − n)
   
   [INT_GE_CALCULATE]  Theorem
      
      ⊢ ∀x y. x ≥ y ⇔ y ≤ x
   
   [INT_GE_REDUCE]  Theorem
      
      ⊢ ∀n m.
          (0 ≥ 0 ⇔ T) ∧ (&NUMERAL n ≥ 0 ⇔ T) ∧
          (-&NUMERAL (BIT1 n) ≥ 0 ⇔ F) ∧ (-&NUMERAL (BIT2 n) ≥ 0 ⇔ F) ∧
          (0 ≥ &NUMERAL (BIT1 n) ⇔ F) ∧ (0 ≥ &NUMERAL (BIT2 n) ⇔ F) ∧
          (0 ≥ -&NUMERAL (BIT1 n) ⇔ T) ∧ (0 ≥ -&NUMERAL (BIT2 n) ⇔ T) ∧
          (&NUMERAL m ≥ &NUMERAL n ⇔ n ≤ m) ∧
          (-&NUMERAL (BIT1 m) ≥ &NUMERAL n ⇔ F) ∧
          (-&NUMERAL (BIT2 m) ≥ &NUMERAL n ⇔ F) ∧
          (&NUMERAL m ≥ -&NUMERAL n ⇔ T) ∧
          (-&NUMERAL m ≥ -&NUMERAL n ⇔ m ≤ n)
   
   [INT_GT_CALCULATE]  Theorem
      
      ⊢ ∀x y. x > y ⇔ y < x
   
   [INT_GT_REDUCE]  Theorem
      
      ⊢ ∀n m.
          (&NUMERAL (BIT1 n) > 0 ⇔ T) ∧ (&NUMERAL (BIT2 n) > 0 ⇔ T) ∧
          (0 > 0 ⇔ F) ∧ (-&NUMERAL n > 0 ⇔ F) ∧ (0 > &NUMERAL n ⇔ F) ∧
          (0 > -&NUMERAL (BIT1 n) ⇔ T) ∧ (0 > -&NUMERAL (BIT2 n) ⇔ T) ∧
          (&NUMERAL m > &NUMERAL n ⇔ n < m) ∧
          (&NUMERAL m > -&NUMERAL (BIT1 n) ⇔ T) ∧
          (&NUMERAL m > -&NUMERAL (BIT2 n) ⇔ T) ∧
          (-&NUMERAL m > &NUMERAL n ⇔ F) ∧
          (-&NUMERAL m > -&NUMERAL n ⇔ m < n)
   
   [INT_INJ]  Theorem
      
      ⊢ ∀m n. &m = &n ⇔ m = n
   
   [INT_LDISTRIB]  Theorem
      
      ⊢ ∀z y x. x * (y + z) = x * y + x * z
   
   [INT_LE]  Theorem
      
      ⊢ ∀m n. &m ≤ &n ⇔ m ≤ n
   
   [INT_LESS_MOD]  Theorem
      
      ⊢ ∀i j. 0 ≤ i ∧ i < j ⇒ i % j = i
   
   [INT_LET_ADD]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 < y ⇒ 0 < x + y
   
   [INT_LET_ADD2]  Theorem
      
      ⊢ ∀w x y z. w ≤ x ∧ y < z ⇒ w + y < x + z
   
   [INT_LET_ANTISYM]  Theorem
      
      ⊢ ∀x y. ¬(x < y ∧ y ≤ x)
   
   [INT_LET_TOTAL]  Theorem
      
      ⊢ ∀x y. x ≤ y ∨ y < x
   
   [INT_LET_TRANS]  Theorem
      
      ⊢ ∀x y z. x ≤ y ∧ y < z ⇒ x < z
   
   [INT_LE_01]  Theorem
      
      ⊢ 0 ≤ 1
   
   [INT_LE_ADD]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x + y
   
   [INT_LE_ADD2]  Theorem
      
      ⊢ ∀w x y z. w ≤ x ∧ y ≤ z ⇒ w + y ≤ x + z
   
   [INT_LE_ADDL]  Theorem
      
      ⊢ ∀x y. y ≤ x + y ⇔ 0 ≤ x
   
   [INT_LE_ADDR]  Theorem
      
      ⊢ ∀x y. x ≤ x + y ⇔ 0 ≤ y
   
   [INT_LE_ANTISYM]  Theorem
      
      ⊢ ∀x y. x ≤ y ∧ y ≤ x ⇔ x = y
   
   [INT_LE_CALCULATE]  Theorem
      
      ⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y
   
   [INT_LE_DOUBLE]  Theorem
      
      ⊢ ∀x. 0 ≤ x + x ⇔ 0 ≤ x
   
   [INT_LE_LADD]  Theorem
      
      ⊢ ∀x y z. x + y ≤ x + z ⇔ y ≤ z
   
   [INT_LE_LT]  Theorem
      
      ⊢ ∀x y. x ≤ y ⇔ x < y ∨ x = y
   
   [INT_LE_LT1]  Theorem
      
      ⊢ x ≤ y ⇔ x < y + 1
   
   [INT_LE_MONO]  Theorem
      
      ⊢ ∀x y z. 0 < x ⇒ (x * y ≤ x * z ⇔ y ≤ z)
   
   [INT_LE_MUL]  Theorem
      
      ⊢ ∀x y. 0 ≤ x ∧ 0 ≤ y ⇒ 0 ≤ x * y
   
   [INT_LE_NEG]  Theorem
      
      ⊢ ∀x y. -x ≤ -y ⇔ y ≤ x
   
   [INT_LE_NEGL]  Theorem
      
      ⊢ ∀x. -x ≤ x ⇔ 0 ≤ x
   
   [INT_LE_NEGR]  Theorem
      
      ⊢ ∀x. x ≤ -x ⇔ x ≤ 0
   
   [INT_LE_NEGTOTAL]  Theorem
      
      ⊢ ∀x. 0 ≤ x ∨ 0 ≤ -x
   
   [INT_LE_RADD]  Theorem
      
      ⊢ ∀x y z. x + z ≤ y + z ⇔ x ≤ y
   
   [INT_LE_REDUCE]  Theorem
      
      ⊢ ∀n m.
          (0 ≤ 0 ⇔ T) ∧ (0 ≤ &NUMERAL n ⇔ T) ∧
          (0 ≤ -&NUMERAL (BIT1 n) ⇔ F) ∧ (0 ≤ -&NUMERAL (BIT2 n) ⇔ F) ∧
          (&NUMERAL (BIT1 n) ≤ 0 ⇔ F) ∧ (&NUMERAL (BIT2 n) ≤ 0 ⇔ F) ∧
          (-&NUMERAL (BIT1 n) ≤ 0 ⇔ T) ∧ (-&NUMERAL (BIT2 n) ≤ 0 ⇔ T) ∧
          (&NUMERAL n ≤ &NUMERAL m ⇔ n ≤ m) ∧
          (&NUMERAL n ≤ -&NUMERAL (BIT1 m) ⇔ F) ∧
          (&NUMERAL n ≤ -&NUMERAL (BIT2 m) ⇔ F) ∧
          (-&NUMERAL n ≤ &NUMERAL m ⇔ T) ∧
          (-&NUMERAL n ≤ -&NUMERAL m ⇔ m ≤ n)
   
   [INT_LE_REFL]  Theorem
      
      ⊢ ∀x. x ≤ x
   
   [INT_LE_SQUARE]  Theorem
      
      ⊢ ∀x. 0 ≤ x * x
   
   [INT_LE_SUB_LADD]  Theorem
      
      ⊢ ∀x y z. x ≤ y − z ⇔ x + z ≤ y
   
   [INT_LE_SUB_RADD]  Theorem
      
      ⊢ ∀x y z. x − y ≤ z ⇔ x ≤ z + y
   
   [INT_LE_TOTAL]  Theorem
      
      ⊢ ∀x y. x ≤ y ∨ y ≤ x
   
   [INT_LE_TRANS]  Theorem
      
      ⊢ ∀x y z. x ≤ y ∧ y ≤ z ⇒ x ≤ z
   
   [INT_LNEG_UNIQ]  Theorem
      
      ⊢ ∀x y. x + y = 0 ⇔ x = -y
   
   [INT_LT]  Theorem
      
      ⊢ ∀m n. &m < &n ⇔ m < n
   
   [INT_LTE_ADD]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 ≤ y ⇒ 0 < x + y
   
   [INT_LTE_ADD2]  Theorem
      
      ⊢ ∀w x y z. w < x ∧ y ≤ z ⇒ w + y < x + z
   
   [INT_LTE_ANTSYM]  Theorem
      
      ⊢ ∀x y. ¬(x ≤ y ∧ y < x)
   
   [INT_LTE_TOTAL]  Theorem
      
      ⊢ ∀x y. x < y ∨ y ≤ x
   
   [INT_LTE_TRANS]  Theorem
      
      ⊢ ∀x y z. x < y ∧ y ≤ z ⇒ x < z
   
   [INT_LT_01]  Theorem
      
      ⊢ 0 < 1
   
   [INT_LT_ADD]  Theorem
      
      ⊢ ∀x y. 0 < x ∧ 0 < y ⇒ 0 < x + y
   
   [INT_LT_ADD1]  Theorem
      
      ⊢ ∀x y. x ≤ y ⇒ x < y + 1
   
   [INT_LT_ADD2]  Theorem
      
      ⊢ ∀w x y z. w < x ∧ y < z ⇒ w + y < x + z
   
   [INT_LT_ADDL]  Theorem
      
      ⊢ ∀x y. y < x + y ⇔ 0 < x
   
   [INT_LT_ADDNEG]  Theorem
      
      ⊢ ∀x y z. y < x + -z ⇔ y + z < x
   
   [INT_LT_ADDNEG2]  Theorem
      
      ⊢ ∀x y z. x + -y < z ⇔ x < z + y
   
   [INT_LT_ADDR]  Theorem
      
      ⊢ ∀x y. x < x + y ⇔ 0 < y
   
   [INT_LT_ADD_SUB]  Theorem
      
      ⊢ ∀x y z. x + y < z ⇔ x < z − y
   
   [INT_LT_ANTISYM]  Theorem
      
      ⊢ ∀x y. ¬(x < y ∧ y < x)
   
   [INT_LT_CALCULATE]  Theorem
      
      ⊢ ∀n m.
          (&n < &m ⇔ n < m) ∧ (-&n < -&m ⇔ m < n) ∧
          (-&n < &m ⇔ n ≠ 0 ∨ m ≠ 0) ∧ (&n < -&m ⇔ F)
   
   [INT_LT_GT]  Theorem
      
      ⊢ ∀x y. x < y ⇒ ¬(y < x)
   
   [INT_LT_IMP_LE]  Theorem
      
      ⊢ ∀x y. x < y ⇒ x ≤ y
   
   [INT_LT_IMP_NE]  Theorem
      
      ⊢ ∀x y. x < y ⇒ x ≠ y
   
   [INT_LT_LADD]  Theorem
      
      ⊢ ∀x y z. x + y < x + z ⇔ y < z
   
   [INT_LT_LADD_IMP]  Theorem
      
      ⊢ ∀x y z. y < z ⇒ x + y < x + z
   
   [INT_LT_LE]  Theorem
      
      ⊢ ∀x y. x < y ⇔ x ≤ y ∧ x ≠ y
   
   [INT_LT_LE1]  Theorem
      
      ⊢ x < y ⇔ x + 1 ≤ y
   
   [INT_LT_MONO]  Theorem
      
      ⊢ ∀x y z. 0 < x ⇒ (x * y < x * z ⇔ y < z)
   
   [INT_LT_MUL]  Theorem
      
      ⊢ ∀x y. int_0 < x ∧ int_0 < y ⇒ int_0 < x * y
   
   [INT_LT_MUL2]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          0 ≤ x1 ∧ 0 ≤ y1 ∧ x1 < x2 ∧ y1 < y2 ⇒ x1 * y1 < x2 * y2
   
   [INT_LT_NEG]  Theorem
      
      ⊢ ∀x y. -x < -y ⇔ y < x
   
   [INT_LT_NEGTOTAL]  Theorem
      
      ⊢ ∀x. x = 0 ∨ 0 < x ∨ 0 < -x
   
   [INT_LT_NZ]  Theorem
      
      ⊢ ∀n. &n ≠ 0 ⇔ 0 < &n
   
   [INT_LT_RADD]  Theorem
      
      ⊢ ∀x y z. x + z < y + z ⇔ x < y
   
   [INT_LT_REDUCE]  Theorem
      
      ⊢ ∀n m.
          (0 < &NUMERAL (BIT1 n) ⇔ T) ∧ (0 < &NUMERAL (BIT2 n) ⇔ T) ∧
          (0 < 0 ⇔ F) ∧ (0 < -&NUMERAL n ⇔ F) ∧ (&NUMERAL n < 0 ⇔ F) ∧
          (-&NUMERAL (BIT1 n) < 0 ⇔ T) ∧ (-&NUMERAL (BIT2 n) < 0 ⇔ T) ∧
          (&NUMERAL n < &NUMERAL m ⇔ n < m) ∧
          (-&NUMERAL (BIT1 n) < &NUMERAL m ⇔ T) ∧
          (-&NUMERAL (BIT2 n) < &NUMERAL m ⇔ T) ∧
          (&NUMERAL n < -&NUMERAL m ⇔ F) ∧
          (-&NUMERAL n < -&NUMERAL m ⇔ m < n)
   
   [INT_LT_REFL]  Theorem
      
      ⊢ ∀x. ¬(x < x)
   
   [INT_LT_SUB_LADD]  Theorem
      
      ⊢ ∀x y z. x < y − z ⇔ x + z < y
   
   [INT_LT_SUB_RADD]  Theorem
      
      ⊢ ∀x y z. x − y < z ⇔ x < z + y
   
   [INT_LT_TOTAL]  Theorem
      
      ⊢ ∀x y. x = y ∨ x < y ∨ y < x
   
   [INT_LT_TRANS]  Theorem
      
      ⊢ ∀x y z. x < y ∧ y < z ⇒ x < z
   
   [INT_MAX_LT]  Theorem
      
      ⊢ ∀x y z. int_max x y < z ⇒ x < z ∧ y < z
   
   [INT_MAX_NUM]  Theorem
      
      ⊢ ∀m n. int_max (&m) (&n) = &MAX m n
   
   [INT_MIN_LT]  Theorem
      
      ⊢ ∀x y z. x < int_min y z ⇒ x < y ∧ x < z
   
   [INT_MIN_NUM]  Theorem
      
      ⊢ ∀m n. int_min (&m) (&n) = &MIN m n
   
   [INT_MOD]  Theorem
      
      ⊢ ∀n m. m ≠ 0 ⇒ &n % &m = &(n MOD m)
   
   [INT_MOD0]  Theorem
      
      ⊢ ∀p. p ≠ 0 ⇒ 0 % p = 0
   
   [INT_MOD_1]  Theorem
      
      ⊢ ∀i. i % 1 = 0
   
   [INT_MOD_ADD_MULTIPLES]  Theorem
      
      ⊢ k ≠ 0 ⇒ (q * k + r) % k = r % k
   
   [INT_MOD_BOUNDS]  Theorem
      
      ⊢ ∀p q.
          q ≠ 0 ⇒
          if q < 0 then q < p % q ∧ p % q ≤ 0 else 0 ≤ p % q ∧ p % q < q
   
   [INT_MOD_CALCULATE]  Theorem
      
      ⊢ (∀n m. m ≠ 0 ⇒ &n % &m = &(n MOD m)) ∧
        (∀p q. q ≠ 0 ⇒ p % -q = -(-p % q)) ∧ (∀x. --x = x) ∧
        (∀m n. &m = &n ⇔ m = n) ∧ ∀x. -x = 0 ⇔ x = 0
   
   [INT_MOD_COMMON_FACTOR]  Theorem
      
      ⊢ ∀p. p ≠ 0 ⇒ ∀q. (q * p) % p = 0
   
   [INT_MOD_EMOD]  Theorem
      
      ⊢ ∀i j. j ≠ 0 ⇒ i % j = if 0 < j then emod i j else -emod (-i) j
   
   [INT_MOD_EQ0]  Theorem
      
      ⊢ ∀q. q ≠ 0 ⇒ ∀p. p % q = 0 ⇔ ∃k. p = k * q
   
   [INT_MOD_FORALL_P]  Theorem
      
      ⊢ ∀P x c.
          c ≠ 0 ⇒
          (P (x % c) ⇔
           ∀q r.
             x = q * c + r ∧
             (c < 0 ∧ c < r ∧ r ≤ 0 ∨ ¬(c < 0) ∧ 0 ≤ r ∧ r < c) ⇒
             P r)
   
   [INT_MOD_ID]  Theorem
      
      ⊢ ∀i. i ≠ 0 ⇒ i % i = 0
   
   [INT_MOD_MINUS1]  Theorem
      
      ⊢ ∀n. 0 < n ⇒ -1 % n = n − 1
   
   [INT_MOD_MOD]  Theorem
      
      ⊢ k ≠ 0 ⇒ j % k % k = j % k
   
   [INT_MOD_NEG]  Theorem
      
      ⊢ ∀p q. q ≠ 0 ⇒ p % -q = -(-p % q)
   
   [INT_MOD_NEG_NUMERATOR]  Theorem
      
      ⊢ k ≠ 0 ⇒ -x % k = (k − x) % k
   
   [INT_MOD_P]  Theorem
      
      ⊢ ∀P x c.
          c ≠ 0 ⇒
          (P (x % c) ⇔
           ∃k r.
             x = k * c + r ∧
             (c < 0 ∧ c < r ∧ r ≤ 0 ∨ ¬(c < 0) ∧ 0 ≤ r ∧ r < c) ∧ P r)
   
   [INT_MOD_PLUS]  Theorem
      
      ⊢ k ≠ 0 ⇒ (i % k + j % k) % k = (i + j) % k
   
   [INT_MOD_REDUCE]  Theorem
      
      ⊢ ∀m n.
          0 % &NUMERAL (BIT1 n) = 0 ∧ 0 % &NUMERAL (BIT2 n) = 0 ∧
          0 % -&NUMERAL (BIT1 n) = 0 ∧ 0 % -&NUMERAL (BIT2 n) = 0 ∧
          &NUMERAL m % &NUMERAL (BIT1 n) =
          &(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
          &NUMERAL m % &NUMERAL (BIT2 n) =
          &(NUMERAL m MOD NUMERAL (BIT2 n)) ∧
          &NUMERAL m % -&NUMERAL (BIT1 n) =
          -(-&NUMERAL m % &NUMERAL (BIT1 n)) ∧
          &NUMERAL m % -&NUMERAL (BIT2 n) =
          -(-&NUMERAL m % &NUMERAL (BIT2 n)) ∧
          x % &NUMERAL (BIT1 n) =
          x − x / &NUMERAL (BIT1 n) * &NUMERAL (BIT1 n) ∧
          x % &NUMERAL (BIT2 n) =
          x − x / &NUMERAL (BIT2 n) * &NUMERAL (BIT2 n) ∧
          x % -&NUMERAL (BIT1 n) =
          -x / &NUMERAL (BIT1 n) * &NUMERAL (BIT1 n) + x ∧
          x % -&NUMERAL (BIT2 n) =
          -x / &NUMERAL (BIT2 n) * &NUMERAL (BIT2 n) + x
   
   [INT_MOD_SUB]  Theorem
      
      ⊢ k ≠ 0 ⇒ (i % k − j % k) % k = (i − j) % k
   
   [INT_MOD_UNIQUE]  Theorem
      
      ⊢ ∀i j m.
          (∃q. i = q * j + m ∧
               if j < 0 then j < m ∧ m ≤ 0 else 0 ≤ m ∧ m < j) ⇒
          i % j = m
   
   [INT_MUL]  Theorem
      
      ⊢ ∀m n. &m * &n = &(m * n)
   
   [INT_MUL_ASSOC]  Theorem
      
      ⊢ ∀z y x. x * (y * z) = x * y * z
   
   [INT_MUL_CALCULATE]  Theorem
      
      ⊢ (∀m n. &m * &n = &(m * n)) ∧ (∀x y. -x * y = -(x * y)) ∧
        (∀x y. x * -y = -(x * y)) ∧ ∀x. --x = x
   
   [INT_MUL_COMM]  Theorem
      
      ⊢ ∀y x. x * y = y * x
   
   [INT_MUL_DIV]  Theorem
      
      ⊢ ∀p q k. q ≠ 0 ∧ p % q = 0 ⇒ k * p / q = k * (p / q)
   
   [INT_MUL_EQ_1]  Theorem
      
      ⊢ ∀x y. x * y = 1 ⇔ x = 1 ∧ y = 1 ∨ x = -1 ∧ y = -1
   
   [INT_MUL_LID]  Theorem
      
      ⊢ ∀x. 1 * x = x
   
   [INT_MUL_LZERO]  Theorem
      
      ⊢ ∀x. 0 * x = 0
   
   [INT_MUL_QUOT]  Theorem
      
      ⊢ ∀p q k. q ≠ 0 ∧ p rem q = 0 ⇒ k * p quot q = k * (p quot q)
   
   [INT_MUL_REDUCE]  Theorem
      
      ⊢ ∀m n p.
          p * 0 = 0 ∧ 0 * p = 0 ∧
          &NUMERAL m * &NUMERAL n = &NUMERAL (m * n) ∧
          -&NUMERAL m * &NUMERAL n = -&NUMERAL (m * n) ∧
          &NUMERAL m * -&NUMERAL n = -&NUMERAL (m * n) ∧
          -&NUMERAL m * -&NUMERAL n = &NUMERAL (m * n)
   
   [INT_MUL_RID]  Theorem
      
      ⊢ ∀x. x * 1 = x
   
   [INT_MUL_RZERO]  Theorem
      
      ⊢ ∀x. x * 0 = 0
   
   [INT_MUL_SIGN_CASES]  Theorem
      
      ⊢ ∀p q.
          (0 < p * q ⇔ 0 < p ∧ 0 < q ∨ p < 0 ∧ q < 0) ∧
          (p * q < 0 ⇔ 0 < p ∧ q < 0 ∨ p < 0 ∧ 0 < q)
   
   [INT_MUL_SYM]  Theorem
      
      ⊢ ∀y x. x * y = y * x
   
   [INT_NEGNEG]  Theorem
      
      ⊢ ∀x. --x = x
   
   [INT_NEG_0]  Theorem
      
      ⊢ -0 = 0
   
   [INT_NEG_ADD]  Theorem
      
      ⊢ ∀x y. -(x + y) = -x + -y
   
   [INT_NEG_EQ]  Theorem
      
      ⊢ ∀x y. -x = y ⇔ x = -y
   
   [INT_NEG_EQ0]  Theorem
      
      ⊢ ∀x. -x = 0 ⇔ x = 0
   
   [INT_NEG_GE0]  Theorem
      
      ⊢ ∀x. 0 ≤ -x ⇔ x ≤ 0
   
   [INT_NEG_GT0]  Theorem
      
      ⊢ ∀x. 0 < -x ⇔ x < 0
   
   [INT_NEG_LE0]  Theorem
      
      ⊢ ∀x. -x ≤ 0 ⇔ 0 ≤ x
   
   [INT_NEG_LMUL]  Theorem
      
      ⊢ ∀x y. -(x * y) = -x * y
   
   [INT_NEG_LT0]  Theorem
      
      ⊢ ∀x. -x < 0 ⇔ 0 < x
   
   [INT_NEG_MINUS1]  Theorem
      
      ⊢ ∀x. -x = -1 * x
   
   [INT_NEG_MUL2]  Theorem
      
      ⊢ ∀x y. -x * -y = x * y
   
   [INT_NEG_RMUL]  Theorem
      
      ⊢ ∀x y. -(x * y) = x * -y
   
   [INT_NEG_SAME_EQ]  Theorem
      
      ⊢ ∀p. p = -p ⇔ p = 0
   
   [INT_NEG_SUB]  Theorem
      
      ⊢ ∀x y. -(x − y) = y − x
   
   [INT_NOT_LE]  Theorem
      
      ⊢ ∀x y. ¬(x ≤ y) ⇔ y < x
   
   [INT_NOT_LT]  Theorem
      
      ⊢ ∀x y. ¬(x < y) ⇔ y ≤ x
   
   [INT_NUM_CASES]  Theorem
      
      ⊢ ∀p. (∃n. p = &n ∧ n ≠ 0) ∨ (∃n. p = -&n ∧ n ≠ 0) ∨ p = 0
   
   [INT_NZ_IMP_LT]  Theorem
      
      ⊢ ∀n. n ≠ 0 ⇒ 0 < &n
   
   [INT_OF_NUM]  Theorem
      
      ⊢ ∀i. &Num i = i ⇔ 0 ≤ i
   
   [INT_POS]  Theorem
      
      ⊢ ∀n. 0 ≤ &n
   
   [INT_POSSQ]  Theorem
      
      ⊢ ∀x. 0 < x * x ⇔ x ≠ 0
   
   [INT_POS_NZ]  Theorem
      
      ⊢ ∀x. 0 < x ⇒ x ≠ 0
   
   [INT_QUOT]  Theorem
      
      ⊢ ∀p q. q ≠ 0 ⇒ &p quot &q = &(p DIV q)
   
   [INT_QUOT_0]  Theorem
      
      ⊢ ∀q. q ≠ 0 ⇒ 0 quot q = 0
   
   [INT_QUOT_1]  Theorem
      
      ⊢ ∀p. p quot 1 = p
   
   [INT_QUOT_CALCULATE]  Theorem
      
      ⊢ (∀p q. q ≠ 0 ⇒ &p quot &q = &(p DIV q)) ∧
        (∀p q. q ≠ 0 ⇒ -p quot q = -(p quot q) ∧ p quot -q = -(p quot q)) ∧
        (∀m n. &m = &n ⇔ m = n) ∧ (∀x. -x = 0 ⇔ x = 0) ∧ ∀x. --x = x
   
   [INT_QUOT_EDIV]  Theorem
      
      ⊢ ∀i j. j ≠ 0 ⇒ i quot j = if 0 ≤ i then ediv i j else ediv (-i) (-j)
   
   [INT_QUOT_ID]  Theorem
      
      ⊢ ∀p. p ≠ 0 ⇒ p quot p = 1
   
   [INT_QUOT_NEG]  Theorem
      
      ⊢ ∀p q. q ≠ 0 ⇒ -p quot q = -(p quot q) ∧ p quot -q = -(p quot q)
   
   [INT_QUOT_REDUCE]  Theorem
      
      ⊢ ∀m n.
          0 quot &NUMERAL (BIT1 n) = 0 ∧ 0 quot &NUMERAL (BIT2 n) = 0 ∧
          &NUMERAL m quot &NUMERAL (BIT1 n) =
          &(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
          &NUMERAL m quot &NUMERAL (BIT2 n) =
          &(NUMERAL m DIV NUMERAL (BIT2 n)) ∧
          -&NUMERAL m quot &NUMERAL (BIT1 n) =
          -&(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
          -&NUMERAL m quot &NUMERAL (BIT2 n) =
          -&(NUMERAL m DIV NUMERAL (BIT2 n)) ∧
          &NUMERAL m quot -&NUMERAL (BIT1 n) =
          -&(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
          &NUMERAL m quot -&NUMERAL (BIT2 n) =
          -&(NUMERAL m DIV NUMERAL (BIT2 n)) ∧
          -&NUMERAL m quot -&NUMERAL (BIT1 n) =
          &(NUMERAL m DIV NUMERAL (BIT1 n)) ∧
          -&NUMERAL m quot -&NUMERAL (BIT2 n) =
          &(NUMERAL m DIV NUMERAL (BIT2 n))
   
   [INT_QUOT_UNIQUE]  Theorem
      
      ⊢ ∀p q k.
          (∃r. p = k * q + r ∧ (if 0 < p then 0 ≤ r else r ≤ 0) ∧
               ABS r < ABS q) ⇒
          p quot q = k
   
   [INT_RDISTRIB]  Theorem
      
      ⊢ ∀x y z. (x + y) * z = x * z + y * z
   
   [INT_REM]  Theorem
      
      ⊢ ∀p q. q ≠ 0 ⇒ &p rem &q = &(p MOD q)
   
   [INT_REM0]  Theorem
      
      ⊢ ∀q. q ≠ 0 ⇒ 0 rem q = 0
   
   [INT_REMQUOT]  Theorem
      
      ⊢ ∀q. q ≠ 0 ⇒
            ∀p. p = p quot q * q + p rem q ∧
                (if 0 < p then 0 ≤ p rem q else p rem q ≤ 0) ∧
                ABS (p rem q) < ABS q
   
   [INT_REM_CALCULATE]  Theorem
      
      ⊢ (∀p q. q ≠ 0 ⇒ &p rem &q = &(p MOD q)) ∧
        (∀p q. q ≠ 0 ⇒ -p rem q = -(p rem q) ∧ p rem -q = p rem q) ∧
        (∀x. --x = x) ∧ (∀m n. &m = &n ⇔ m = n) ∧ ∀x. -x = 0 ⇔ x = 0
   
   [INT_REM_COMMON_FACTOR]  Theorem
      
      ⊢ ∀p. p ≠ 0 ⇒ ∀q. (q * p) rem p = 0
   
   [INT_REM_EMOD]  Theorem
      
      ⊢ ∀i j. j ≠ 0 ⇒ i rem j = if 0 ≤ i then emod i j else -emod (-i) j
   
   [INT_REM_EQ0]  Theorem
      
      ⊢ ∀q. q ≠ 0 ⇒ ∀p. p rem q = 0 ⇔ ∃k. p = k * q
   
   [INT_REM_EQ_MOD]  Theorem
      
      ⊢ ∀i n.
          0 < n ⇒ i rem n = if i < 0 then (i − 1) % n − n + 1 else i % n
   
   [INT_REM_ID]  Theorem
      
      ⊢ ∀p. p ≠ 0 ⇒ p rem p = 0
   
   [INT_REM_NEG]  Theorem
      
      ⊢ ∀p q. q ≠ 0 ⇒ -p rem q = -(p rem q) ∧ p rem -q = p rem q
   
   [INT_REM_REDUCE]  Theorem
      
      ⊢ ∀m n.
          0 rem &NUMERAL (BIT1 n) = 0 ∧ 0 rem &NUMERAL (BIT2 n) = 0 ∧
          &NUMERAL m rem &NUMERAL (BIT1 n) =
          &(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
          &NUMERAL m rem &NUMERAL (BIT2 n) =
          &(NUMERAL m MOD NUMERAL (BIT2 n)) ∧
          -&NUMERAL m rem &NUMERAL (BIT1 n) =
          -&(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
          -&NUMERAL m rem &NUMERAL (BIT2 n) =
          -&(NUMERAL m MOD NUMERAL (BIT2 n)) ∧
          &NUMERAL m rem -&NUMERAL (BIT1 n) =
          &(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
          &NUMERAL m rem -&NUMERAL (BIT2 n) =
          &(NUMERAL m MOD NUMERAL (BIT2 n)) ∧
          -&NUMERAL m rem -&NUMERAL (BIT1 n) =
          -&(NUMERAL m MOD NUMERAL (BIT1 n)) ∧
          -&NUMERAL m rem -&NUMERAL (BIT2 n) =
          -&(NUMERAL m MOD NUMERAL (BIT2 n))
   
   [INT_REM_UNIQUE]  Theorem
      
      ⊢ ∀p q r.
          ABS r < ABS q ∧ (if 0 < p then 0 ≤ r else r ≤ 0) ∧
          (∃k. p = k * q + r) ⇒
          p rem q = r
   
   [INT_RNEG_UNIQ]  Theorem
      
      ⊢ ∀x y. x + y = 0 ⇔ y = -x
   
   [INT_SUB]  Theorem
      
      ⊢ ∀n m. m ≤ n ⇒ &n − &m = &(n − m)
   
   [INT_SUB_0]  Theorem
      
      ⊢ ∀x y. x − y = 0 ⇔ x = y
   
   [INT_SUB_ABS_TRIANGLE]  Theorem
      
      ⊢ ABS i − ABS j ≤ ABS (i − j)
   
   [INT_SUB_ADD]  Theorem
      
      ⊢ ∀x y. x − y + y = x
   
   [INT_SUB_ADD2]  Theorem
      
      ⊢ ∀x y. y + (x − y) = x
   
   [INT_SUB_CALCULATE]  Theorem
      
      ⊢ ∀x y. x − y = x + -y
   
   [INT_SUB_LDISTRIB]  Theorem
      
      ⊢ ∀x y z. x * (y − z) = x * y − x * z
   
   [INT_SUB_LE]  Theorem
      
      ⊢ ∀x y. 0 ≤ x − y ⇔ y ≤ x
   
   [INT_SUB_LNEG]  Theorem
      
      ⊢ ∀x y. -x − y = -(x + y)
   
   [INT_SUB_LT]  Theorem
      
      ⊢ ∀x y. 0 < x − y ⇔ y < x
   
   [INT_SUB_LZERO]  Theorem
      
      ⊢ ∀x. 0 − x = -x
   
   [INT_SUB_NEG2]  Theorem
      
      ⊢ ∀x y. -x − -y = y − x
   
   [INT_SUB_RDISTRIB]  Theorem
      
      ⊢ ∀x y z. (x − y) * z = x * z − y * z
   
   [INT_SUB_REDUCE]  Theorem
      
      ⊢ ∀m n p.
          p − 0 = p ∧ 0 − p = -p ∧
          &NUMERAL m − &NUMERAL n = &NUMERAL m + -&NUMERAL n ∧
          -&NUMERAL m − &NUMERAL n = -&NUMERAL m + -&NUMERAL n ∧
          &NUMERAL m − -&NUMERAL n = &NUMERAL m + &NUMERAL n ∧
          -&NUMERAL m − -&NUMERAL n = -&NUMERAL m + &NUMERAL n
   
   [INT_SUB_REFL]  Theorem
      
      ⊢ ∀x. x − x = 0
   
   [INT_SUB_RNEG]  Theorem
      
      ⊢ ∀x y. x − -y = x + y
   
   [INT_SUB_RZERO]  Theorem
      
      ⊢ ∀x. x − 0 = x
   
   [INT_SUB_SUB]  Theorem
      
      ⊢ ∀x y. x − y − x = -y
   
   [INT_SUB_SUB2]  Theorem
      
      ⊢ ∀x y. x − (x − y) = y
   
   [INT_SUB_TRIANGLE]  Theorem
      
      ⊢ ∀a b c. a − b + (b − c) = a − c
   
   [INT_SUMSQ]  Theorem
      
      ⊢ ∀x y. x * x + y * y = 0 ⇔ x = 0 ∧ y = 0
   
   [LE_NUM_OF_INT]  Theorem
      
      ⊢ ∀n i. &n ≤ i ⇒ n ≤ Num i
   
   [LT_ADD2]  Theorem
      
      ⊢ ∀x1 x2 y1 y2. x1 < y1 ∧ x2 < y2 ⇒ x1 + x2 < y1 + y2
   
   [LT_ADDL]  Theorem
      
      ⊢ ∀x y. x < x + y ⇔ 0 < y
   
   [LT_ADDR]  Theorem
      
      ⊢ ∀x y. ¬(x + y < x)
   
   [LT_LADD]  Theorem
      
      ⊢ ∀x y z. x + y < x + z ⇔ y < z
   
   [NUM_EQ0]  Theorem
      
      ⊢ Num i = 0 ⇔ i = 0
   
   [NUM_INT_ADD]  Theorem
      
      ⊢ ∀m n. m + n = Num (&m + &n)
   
   [NUM_INT_EDIV]  Theorem
      
      ⊢ ∀n m. m ≠ 0 ⇒ n DIV m = Num (ediv (&n) (&m))
   
   [NUM_INT_EMOD]  Theorem
      
      ⊢ ∀n m. m ≠ 0 ⇒ n MOD m = Num (emod (&n) (&m))
   
   [NUM_INT_MUL]  Theorem
      
      ⊢ ∀m n. m * n = Num (&m * &n)
   
   [NUM_INT_SUB]  Theorem
      
      ⊢ ∀m n. m − n = if &m ≤ &n then 0 else Num (&m − &n)
   
   [NUM_LT]  Theorem
      
      ⊢ 0 ≤ x ∧ 0 ≤ y ⇒ (Num x < Num y ⇔ x < y)
   
   [NUM_NEGINT_EXISTS]  Theorem
      
      ⊢ ∀i. i ≤ 0 ⇒ ∃n. i = -&n
   
   [NUM_OF_INT]  Theorem
      
      ⊢ ∀n. Num (&n) = n
   
   [NUM_OF_NEG_INT]  Theorem
      
      ⊢ ∀n. Num (-&n) = n
   
   [NUM_POSINT]  Theorem
      
      ⊢ ∀i. 0 ≤ i ⇒ ∃!n. i = &n
   
   [NUM_POSINT_EX]  Theorem
      
      ⊢ ∀t. ¬(t < int_0) ⇒ ∃n. t = &n
   
   [NUM_POSINT_EXISTS]  Theorem
      
      ⊢ ∀i. 0 ≤ i ⇒ ∃n. i = &n
   
   [NUM_POSTINT_EX]  Theorem
      
      ⊢ ∀t. ¬(t tint_lt tint_0) ⇒ ∃n. t tint_eq tint_of_num n
   
   [Num_EQ]  Theorem
      
      ⊢ Num a = Num b ⇔ a = b ∨ a = -b
   
   [Num_EQ_ABS]  Theorem
      
      ⊢ ∀i. &Num i = ABS i
   
   [Num_neg]  Theorem
      
      ⊢ Num (-a) = Num a
   
   [TINT_10]  Theorem
      
      ⊢ ¬(tint_1 tint_eq tint_0)
   
   [TINT_ADD_ASSOC]  Theorem
      
      ⊢ ∀z y x. x tint_add (y tint_add z) = x tint_add y tint_add z
   
   [TINT_ADD_LID]  Theorem
      
      ⊢ ∀x. tint_0 tint_add x tint_eq x
   
   [TINT_ADD_LINV]  Theorem
      
      ⊢ ∀x. tint_neg x tint_add x tint_eq tint_0
   
   [TINT_ADD_SYM]  Theorem
      
      ⊢ ∀y x. x tint_add y = y tint_add x
   
   [TINT_ADD_WELLDEF]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          x1 tint_eq x2 ∧ y1 tint_eq y2 ⇒
          x1 tint_add y1 tint_eq x2 tint_add y2
   
   [TINT_ADD_WELLDEFR]  Theorem
      
      ⊢ ∀x1 x2 y. x1 tint_eq x2 ⇒ x1 tint_add y tint_eq x2 tint_add y
   
   [TINT_EQ_AP]  Theorem
      
      ⊢ ∀p q. p = q ⇒ p tint_eq q
   
   [TINT_EQ_EQUIV]  Theorem
      
      ⊢ ∀p q. p tint_eq q ⇔ $tint_eq p = $tint_eq q
   
   [TINT_EQ_REFL]  Theorem
      
      ⊢ ∀x. x tint_eq x
   
   [TINT_EQ_SYM]  Theorem
      
      ⊢ ∀x y. x tint_eq y ⇔ y tint_eq x
   
   [TINT_EQ_TRANS]  Theorem
      
      ⊢ ∀x y z. x tint_eq y ∧ y tint_eq z ⇒ x tint_eq z
   
   [TINT_INJ]  Theorem
      
      ⊢ ∀m n. tint_of_num m tint_eq tint_of_num n ⇔ m = n
   
   [TINT_LDISTRIB]  Theorem
      
      ⊢ ∀z y x.
          x tint_mul (y tint_add z) = x tint_mul y tint_add x tint_mul z
   
   [TINT_LT_ADD]  Theorem
      
      ⊢ ∀x y z. y tint_lt z ⇒ x tint_add y tint_lt x tint_add z
   
   [TINT_LT_MUL]  Theorem
      
      ⊢ ∀x y.
          tint_0 tint_lt x ∧ tint_0 tint_lt y ⇒ tint_0 tint_lt x tint_mul y
   
   [TINT_LT_REFL]  Theorem
      
      ⊢ ∀x. ¬(x tint_lt x)
   
   [TINT_LT_TOTAL]  Theorem
      
      ⊢ ∀x y. x tint_eq y ∨ x tint_lt y ∨ y tint_lt x
   
   [TINT_LT_TRANS]  Theorem
      
      ⊢ ∀x y z. x tint_lt y ∧ y tint_lt z ⇒ x tint_lt z
   
   [TINT_LT_WELLDEF]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          x1 tint_eq x2 ∧ y1 tint_eq y2 ⇒ (x1 tint_lt y1 ⇔ x2 tint_lt y2)
   
   [TINT_LT_WELLDEFL]  Theorem
      
      ⊢ ∀x y1 y2. y1 tint_eq y2 ⇒ (x tint_lt y1 ⇔ x tint_lt y2)
   
   [TINT_LT_WELLDEFR]  Theorem
      
      ⊢ ∀x1 x2 y. x1 tint_eq x2 ⇒ (x1 tint_lt y ⇔ x2 tint_lt y)
   
   [TINT_MUL_ASSOC]  Theorem
      
      ⊢ ∀z y x. x tint_mul (y tint_mul z) = x tint_mul y tint_mul z
   
   [TINT_MUL_LID]  Theorem
      
      ⊢ ∀x. tint_1 tint_mul x tint_eq x
   
   [TINT_MUL_SYM]  Theorem
      
      ⊢ ∀y x. x tint_mul y = y tint_mul x
   
   [TINT_MUL_WELLDEF]  Theorem
      
      ⊢ ∀x1 x2 y1 y2.
          x1 tint_eq x2 ∧ y1 tint_eq y2 ⇒
          x1 tint_mul y1 tint_eq x2 tint_mul y2
   
   [TINT_MUL_WELLDEFR]  Theorem
      
      ⊢ ∀x1 x2 y. x1 tint_eq x2 ⇒ x1 tint_mul y tint_eq x2 tint_mul y
   
   [TINT_NEG_WELLDEF]  Theorem
      
      ⊢ ∀x1 x2. x1 tint_eq x2 ⇒ tint_neg x1 tint_eq tint_neg x2
   
   [int_ABS_REP_CLASS]  Theorem
      
      ⊢ (∀a. int_ABS_CLASS (int_REP_CLASS a) = a) ∧
        ∀c. (∃r. r tint_eq r ∧ c = $tint_eq r) ⇔
            int_REP_CLASS (int_ABS_CLASS c) = c
   
   [int_QUOTIENT]  Theorem
      
      ⊢ QUOTIENT $tint_eq int_ABS int_REP
   
   [int_eq_calculate]  Theorem
      
      ⊢ ∀n m. (&n = -&m ⇔ n = 0 ∧ m = 0) ∧ (-&n = &m ⇔ n = 0 ∧ m = 0)
   
   [num_of_int]  Theorem
      
      ⊢ ∀i. Num i = @n. if 0 ≤ i then i = &n else i = -&n
   
   [tint_of_num_eq]  Theorem
      
      ⊢ ∀n. FST (tint_of_num n) = SND (tint_of_num n) + n
   
   
*)
end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1