Theory "integer"

Signature

Definitions

int_ge

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

int_gt

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

int_le

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

int_sub

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

tint_0

|- tint_0 = (1,1)

tint_1

|- tint_1 = (1 + 1,1)

tint_neg

|- ∀x y. tint_neg (x,y) = (y,x)

tint_add

|- ∀x1 y1 x2 y2. (x1,y1) tint_add (x2,y2) = (x1 + x2,y1 + y2)

tint_mul

|- ∀x1 y1 x2 y2.
     (x1,y1) tint_mul (x2,y2) = (x1 * x2 + y1 * y2,x1 * y2 + y1 * x2)

tint_lt

|- ∀x1 y1 x2 y2. tint_lt (x1,y1) (x2,y2) ⇔ x1 + y2 < x2 + y1

tint_eq

|- ∀x1 y1 x2 y2. tint_eq (x1,y1) (x2,y2) ⇔ (x1 + y2 = x2 + y1)

tint_of_num

|- (tint_of_num 0 = tint_0) ∧
   ∀n. tint_of_num (SUC n) = tint_of_num n tint_add tint_1

int_TY_DEF

|- ∃rep. TYPE_DEFINITION (λc. ∃r. tint_eq r r ∧ (c = tint_eq r)) rep

int_bijections

|- (∀a. int_ABS_CLASS (int_REP_CLASS a) = a) ∧
   ∀r.
     (λc. ∃r. tint_eq r r ∧ (c = tint_eq r)) r ⇔
     (int_REP_CLASS (int_ABS_CLASS r) = r)

int_REP_def

|- ∀a. int_REP a = $@ (int_REP_CLASS a)

int_ABS_def

|- ∀r. int_ABS r = int_ABS_CLASS (tint_eq r)

int_0

|- int_0 = int_ABS tint_0

int_1

|- int_1 = int_ABS tint_1

int_neg

|- ∀T1. -T1 = int_ABS (tint_neg (int_REP T1))

int_add

|- ∀T1 T2. T1 + T2 = int_ABS (int_REP T1 tint_add int_REP T2)

int_mul

|- ∀T1 T2. T1 * T2 = int_ABS (int_REP T1 tint_mul int_REP T2)

int_lt

|- ∀T1 T2. T1 < T2 ⇔ tint_lt (int_REP T1) (int_REP T2)

Num

|- ∀i. Num i = @n. i = &n

int_div

|- ∀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_mod

|- ∀i j. j ≠ 0 ⇒ (i % j = i − i / j * j)

INT_ABS

|- ∀n. ABS n = if n < 0 then -n else n

int_quot

|- ∀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

|- ∀i j. j ≠ 0 ⇒ (i rem j = i − i quot j * j)

INT_DIVIDES

|- ∀p q. p int_divides q ⇔ ∃m. m * p = q

int_exp

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

INT_MIN

|- ∀x y. int_min x y = if x < y then x else y

INT_MAX

|- ∀x y. int_max x y = if x < y then y else x

LEAST_INT_DEF

|- ∀P. $LEAST_INT P = @i. P i ∧ ∀j. j < i ⇒ ¬P j

Theorems

INT_LT

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

INT_LE

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

INT_POS

|- ∀n. 0 ≤ &n

INT

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

INT_EQ_RMUL

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

INT_EQ_LMUL

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

INT_ENTIRE

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

INT_LT_ADDL

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

INT_LT_ADDR

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

INT_LE_ADDL

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

INT_LE_ADDR

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

INT_LT_IMP_NE

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

INT_NEG_MINUS1

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

INT_NEG_EQ

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

INT_SUB_RDISTRIB

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

INT_SUB_LDISTRIB

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

INT_ADD_SUB

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

INT_SUB_LE

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

INT_SUB_LT

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

INT_NEG_SUB

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

INT_NEG_0

|- -0 = 0

INT_NEG_EQ0

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

INT_LE_NEGR

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

INT_LE_NEGL

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

INT_LE_DOUBLE

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

INT_SUB_0

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

INT_SUB_REFL

|- ∀x. x − x = 0

INT_SUB_ADD2

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

INT_SUB_ADD

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

INT_LT_ADD1

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

INT_LT_ADDNEG2

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

INT_LT_ADDNEG

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

INT_LT_ADD

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

INT_LE_ADD

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

INT_LE_ADD2

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

INT_LT_ADD2

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

INT_LE_RADD

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

INT_LE_LADD

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

INT_LT_01

|- 0 < 1

INT_LE_01

|- 0 ≤ 1

INT_LE_SQUARE

|- ∀x. 0 ≤ x * x

INT_LE_MUL

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

INT_LE_NEGTOTAL

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

INT_LT_NEGTOTAL

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

INT_NEG_GE0

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

INT_NEG_LE0

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

INT_NEG_GT0

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

INT_NEG_LT0

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

INT_LTE_ANTSYM

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

INT_LET_ANTISYM

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

INT_LE_ANTISYM

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

INT_LE_TRANS

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

INT_LET_TRANS

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

INT_LTE_TRANS

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

INT_LT_IMP_LE

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

INT_LT_LE

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

INT_LE_LT

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

INT_LE_REFL

|- ∀x. x ≤ x

INT_LTE_TOTAL

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

INT_LET_TOTAL

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

INT_LE_TOTAL

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

INT_NOT_LE

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

INT_LT_GT

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

INT_LT_ANTISYM

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

INT_NOT_LT

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

INT_LT_RADD

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

INT_LT_LADD

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

INT_NEG_MUL2

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

INT_NEGNEG

|- ∀x. - -x = x

INT_NEG_RMUL

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

INT_NEG_LMUL

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

INT_MUL_RZERO

|- ∀x. x * 0 = 0

INT_MUL_LZERO

|- ∀x. 0 * x = 0

INT_NEG_ADD

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

INT_RNEG_UNIQ

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

INT_LNEG_UNIQ

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

INT_ADD_RID_UNIQ

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

INT_ADD_LID_UNIQ

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

INT_EQ_RADD

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

INT_EQ_LADD

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

INT_RDISTRIB

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

INT_MUL_RID

|- ∀x. x * 1 = x

INT_MUL_LID

|- ∀x. 1 * x = x

INT_ADD_RINV

|- ∀x. x + -x = 0

INT_ADD_LINV

|- ∀x. -x + x = 0

INT_ADD_RID

|- ∀x. x + 0 = x

INT_ADD_LID

|- ∀x. 0 + x = x

INT_1

|- int_1 = 1

INT_0

|- int_0 = 0

NUM_POSINT_EX

|- ∀t. ¬(t < int_0) ⇒ ∃n. t = &n

INT_LT_MUL

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

INT_LT_LADD_IMP

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

INT_LT_TRANS

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

INT_LT_REFL

|- ∀x. ¬(x < x)

INT_LT_TOTAL

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

INT_LDISTRIB

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

INT_MUL_ASSOC

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

INT_ADD_ASSOC

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

INT_MUL_COMM

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

INT_MUL_SYM

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

INT_ADD_COMM

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

INT_ADD_SYM

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

INT_10

|- int_1 ≠ int_0

EQ_LADD

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

EQ_ADDL

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

LT_LADD

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

LT_ADDL

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

LT_ADDR

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

LT_ADD2

|- ∀x1 x2 y1 y2. x1 < y1 ∧ x2 < y2 ⇒ x1 + x2 < y1 + y2

TINT_EQ_REFL

|- ∀x. tint_eq x x

TINT_EQ_SYM

|- ∀x y. tint_eq x y ⇔ tint_eq y x

TINT_EQ_TRANS

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

TINT_EQ_EQUIV

|- ∀p q. tint_eq p q ⇔ (tint_eq p = tint_eq q)

TINT_EQ_AP

|- ∀p q. (p = q) ⇒ tint_eq p q

TINT_10

|- ¬tint_eq tint_1 tint_0

TINT_ADD_SYM

|- ∀x y. x tint_add y = y tint_add x

TINT_MUL_SYM

|- ∀x y. x tint_mul y = y tint_mul x

TINT_ADD_ASSOC

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

TINT_MUL_ASSOC

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

TINT_LDISTRIB

|- ∀x y z. x tint_mul (y tint_add z) = x tint_mul y tint_add x tint_mul z

TINT_ADD_LID

|- ∀x. tint_eq (tint_0 tint_add x) x

TINT_MUL_LID

|- ∀x. tint_eq (tint_1 tint_mul x) x

TINT_ADD_LINV

|- ∀x. tint_eq (tint_neg x tint_add x) tint_0

TINT_LT_TOTAL

|- ∀x y. tint_eq x y ∨ tint_lt x y ∨ tint_lt y x

TINT_LT_REFL

|- ∀x. ¬tint_lt x x

TINT_LT_TRANS

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

TINT_LT_ADD

|- ∀x y z. tint_lt y z ⇒ tint_lt (x tint_add y) (x tint_add z)

TINT_LT_MUL

|- ∀x y. tint_lt tint_0 x ∧ tint_lt tint_0 y ⇒ tint_lt tint_0 (x tint_mul y)

TINT_NEG_WELLDEF

|- ∀x1 x2. tint_eq x1 x2 ⇒ tint_eq (tint_neg x1) (tint_neg x2)

TINT_ADD_WELLDEFR

|- ∀x1 x2 y. tint_eq x1 x2 ⇒ tint_eq (x1 tint_add y) (x2 tint_add y)

TINT_ADD_WELLDEF

|- ∀x1 x2 y1 y2.
     tint_eq x1 x2 ∧ tint_eq y1 y2 ⇒ tint_eq (x1 tint_add y1) (x2 tint_add y2)

TINT_MUL_WELLDEFR

|- ∀x1 x2 y. tint_eq x1 x2 ⇒ tint_eq (x1 tint_mul y) (x2 tint_mul y)

TINT_MUL_WELLDEF

|- ∀x1 x2 y1 y2.
     tint_eq x1 x2 ∧ tint_eq y1 y2 ⇒ tint_eq (x1 tint_mul y1) (x2 tint_mul y2)

TINT_LT_WELLDEFR

|- ∀x1 x2 y. tint_eq x1 x2 ⇒ (tint_lt x1 y ⇔ tint_lt x2 y)

TINT_LT_WELLDEFL

|- ∀x y1 y2. tint_eq y1 y2 ⇒ (tint_lt x y1 ⇔ tint_lt x y2)

TINT_LT_WELLDEF

|- ∀x1 x2 y1 y2.
     tint_eq x1 x2 ∧ tint_eq y1 y2 ⇒ (tint_lt x1 y1 ⇔ tint_lt x2 y2)

tint_of_num_eq

|- ∀n. FST (tint_of_num n) = SND (tint_of_num n) + n

TINT_INJ

|- ∀m n. tint_eq (tint_of_num m) (tint_of_num n) ⇔ (m = n)

NUM_POSTINT_EX

|- ∀t. ¬tint_lt t tint_0 ⇒ ∃n. tint_eq t (tint_of_num n)

int_ABS_REP_CLASS

|- (∀a. int_ABS_CLASS (int_REP_CLASS a) = a) ∧
   ∀c.
     (∃r. tint_eq r r ∧ (c = tint_eq r)) ⇔
     (int_REP_CLASS (int_ABS_CLASS c) = c)

int_QUOTIENT

|- QUOTIENT tint_eq int_ABS int_REP

int_of_num

|- (0 = int_0) ∧ ∀n. &SUC n = &n + int_1

INT_INJ

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

INT_ADD

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

INT_MUL

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

INT_LT_NZ

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

INT_NZ_IMP_LT

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

INT_DOUBLE

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

INT_SUB_SUB

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

INT_LT_ADD_SUB

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

INT_LT_SUB_RADD

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

INT_LT_SUB_LADD

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

INT_LE_SUB_LADD

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

INT_LE_SUB_RADD

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

INT_LT_NEG

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

INT_LE_NEG

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

INT_ADD2_SUB2

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

INT_SUB_LZERO

|- ∀x. 0 − x = -x

INT_SUB_RZERO

|- ∀x. x − 0 = x

INT_LET_ADD2

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

INT_LTE_ADD2

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

INT_LET_ADD

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

INT_LTE_ADD

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

INT_LT_MUL2

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

INT_SUB_LNEG

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

INT_SUB_RNEG

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

INT_SUB_NEG2

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

INT_SUB_TRIANGLE

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

INT_EQ_SUB_LADD

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

INT_EQ_SUB_RADD

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

INT_SUB

|- ∀n m. m ≤ n ⇒ (&n − &m = &(n − m))

INT_SUB_SUB2

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

INT_ADD_SUB2

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

INT_EQ_LMUL2

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

INT_EQ_IMP_LE

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

INT_POS_NZ

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

INT_EQ_RMUL_IMP

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

INT_EQ_LMUL_IMP

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

INT_DIFFSQ

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

INT_POASQ

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

INT_SUMSQ

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

INT_EQ_NEG

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

INT_LT_CALCULATE

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

NUM_POSINT

|- ∀i. 0 ≤ i ⇒ ∃!n. i = &n

NUM_POSINT_EXISTS

|- ∀i. 0 ≤ i ⇒ ∃n. i = &n

NUM_NEGINT_EXISTS

|- ∀i. i ≤ 0 ⇒ ∃n. i = -&n

INT_NUM_CASES

|- ∀p. (∃n. (p = &n) ∧ n ≠ 0) ∨ (∃n. (p = -&n) ∧ n ≠ 0) ∨ (p = 0)

INT_DISCRETE

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

INT_LE_LT1

|- x ≤ y ⇔ x < y + 1

INT_LT_LE1

|- x < y ⇔ x + 1 ≤ y

INT_MUL_EQ_1

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

NUM_OF_INT

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

INT_OF_NUM

|- ∀i. (&Num i = i) ⇔ 0 ≤ i

LE_NUM_OF_INT

|- ∀n i. &n ≤ i ⇒ n ≤ Num i

INT_DIV

|- ∀n m. m ≠ 0 ⇒ (&n / &m = &(n DIV m))

INT_DIV_NEG

|- ∀p q. q ≠ 0 ⇒ (p / -q = -p / q)

INT_DIV_1

|- ∀p. p / 1 = p

INT_DIV_0

|- ∀q. q ≠ 0 ⇒ (0 / q = 0)

INT_DIV_ID

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

INT_MOD_BOUNDS

|- ∀p q.
     q ≠ 0 ⇒ if q < 0 then q < p % q ∧ p % q ≤ 0 else 0 ≤ p % q ∧ p % q < q

INT_DIVISION

|- ∀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_MOD

|- ∀n m. m ≠ 0 ⇒ (&n % &m = &(n MOD m))

INT_MOD_NEG

|- ∀p q. q ≠ 0 ⇒ (p % -q = -(-p % q))

INT_MOD0

|- ∀p. p ≠ 0 ⇒ (0 % p = 0)

INT_DIV_MUL_ID

|- ∀p q. q ≠ 0 ∧ (p % q = 0) ⇒ (p / q * q = p)

INT_DIV_UNIQUE

|- ∀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_MOD_UNIQUE

|- ∀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_MOD_ID

|- ∀i. i ≠ 0 ⇒ (i % i = 0)

INT_MOD_COMMON_FACTOR

|- ∀p. p ≠ 0 ⇒ ∀q. (q * p) % p = 0

INT_DIV_LMUL

|- ∀i j. i ≠ 0 ⇒ (i * j / i = j)

INT_DIV_RMUL

|- ∀i j. i ≠ 0 ⇒ (j * i / i = j)

INT_MOD_EQ0

|- ∀q. q ≠ 0 ⇒ ∀p. (p % q = 0) ⇔ ∃k. p = k * q

INT_MUL_DIV

|- ∀p q k. q ≠ 0 ∧ (p % q = 0) ⇒ (k * p / q = k * (p / q))

INT_ADD_DIV

|- ∀i j k. k ≠ 0 ∧ ((i % k = 0) ∨ (j % k = 0)) ⇒ ((i + j) / k = i / k + j / k)

INT_MOD_ADD_MULTIPLES

|- k ≠ 0 ⇒ ((q * k + r) % k = r % k)

INT_MOD_NEG_NUMERATOR

|- k ≠ 0 ⇒ (-x % k = (k − x) % k)

INT_MOD_PLUS

|- k ≠ 0 ⇒ ((i % k + j % k) % k = (i + j) % k)

INT_MOD_SUB

|- k ≠ 0 ⇒ ((i % k − j % k) % k = (i − j) % k)

INT_MOD_MOD

|- k ≠ 0 ⇒ (j % k % k = j % k)

INT_DIV_P

|- ∀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_MOD_P

|- ∀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_DIV_FORALL_P

|- ∀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_MOD_FORALL_P

|- ∀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_1

|- ∀i. i % 1 = 0

INT_LESS_MOD

|- ∀i j. 0 ≤ i ∧ i < j ⇒ (i % j = i)

INT_MOD_MINUS1

|- ∀n. 0 < n ⇒ (-1 % n = n − 1)

INT_ABS_POS

|- ∀p. 0 ≤ ABS p

INT_ABS_NUM

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

INT_NEG_SAME_EQ

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

INT_ABS_NEG

|- ∀p. ABS (-p) = ABS p

INT_ABS_ABS

|- ∀p. ABS (ABS p) = ABS p

INT_ABS_EQ_ID

|- ∀p. (ABS p = p) ⇔ 0 ≤ p

INT_ABS_MUL

|- ∀p q. ABS p * ABS q = ABS (p * q)

INT_ABS_EQ0

|- ∀p. (ABS p = 0) ⇔ (p = 0)

INT_ABS_LT0

|- ∀p. ¬(ABS p < 0)

INT_ABS_LE0

|- ∀p. ABS p ≤ 0 ⇔ (p = 0)

INT_ABS_LT

|- ∀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_LE

|- ∀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_EQ

|- ∀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_QUOT

|- ∀p q. q ≠ 0 ⇒ (&p quot &q = &(p DIV q))

INT_QUOT_0

|- ∀q. q ≠ 0 ⇒ (0 quot q = 0)

INT_QUOT_1

|- ∀p. p quot 1 = p

INT_QUOT_NEG

|- ∀p q. q ≠ 0 ⇒ (-p quot q = -(p quot q)) ∧ (p quot -q = -(p quot q))

INT_ABS_QUOT

|- ∀p q. q ≠ 0 ⇒ ABS (p quot q * q) ≤ ABS p

INT_QUOT_UNIQUE

|- ∀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_QUOT_ID

|- ∀p. p ≠ 0 ⇒ (p quot p = 1)

INT_REM

|- ∀p q. q ≠ 0 ⇒ (&p rem &q = &(p MOD q))

INT_REMQUOT

|- ∀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_UNIQUE

|- ∀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_REM_NEG

|- ∀p q. q ≠ 0 ⇒ (-p rem q = -(p rem q)) ∧ (p rem -q = p rem q)

INT_REM_ID

|- ∀p. p ≠ 0 ⇒ (p rem p = 0)

INT_REM0

|- ∀q. q ≠ 0 ⇒ (0 rem q = 0)

INT_REM_COMMON_FACTOR

|- ∀p. p ≠ 0 ⇒ ∀q. q * p rem p = 0

INT_REM_EQ0

|- ∀q. q ≠ 0 ⇒ ∀p. (p rem q = 0) ⇔ ∃k. p = k * q

INT_MUL_QUOT

|- ∀p q k. q ≠ 0 ∧ (p rem q = 0) ⇒ (k * p quot q = k * (p quot q))

INT_REM_EQ_MOD

|- ∀i n. 0 < n ⇒ (i rem n = if i < 0 then (i − 1) % n − n + 1 else i % n)

INT_DIVIDES_MOD0

|- ∀p q. p int_divides q ⇔ (q % p = 0) ∧ p ≠ 0 ∨ (p = 0) ∧ (q = 0)

INT_DIVIDES_0

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

INT_DIVIDES_1

|- ∀x. 1 int_divides x ∧ (x int_divides 1 ⇔ (x = 1) ∨ (x = -1))

INT_DIVIDES_REFL

|- ∀x. x int_divides x

INT_DIVIDES_TRANS

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

INT_DIVIDES_MUL

|- ∀p q. p int_divides p * q ∧ p int_divides q * p

INT_DIVIDES_LMUL

|- ∀p q r. p int_divides q ⇒ p int_divides q * r

INT_DIVIDES_RMUL

|- ∀p q r. p int_divides q ⇒ p int_divides r * q

INT_DIVIDES_MUL_BOTH

|- ∀p q r. p ≠ 0 ⇒ (p * q int_divides p * r ⇔ q int_divides r)

INT_DIVIDES_LADD

|- ∀p q r. p int_divides q ⇒ (p int_divides q + r ⇔ p int_divides r)

INT_DIVIDES_RADD

|- ∀p q r. p int_divides q ⇒ (p int_divides r + q ⇔ p int_divides r)

INT_DIVIDES_NEG

|- ∀p q.
     (p int_divides -q ⇔ p int_divides q) ∧
     (-p int_divides q ⇔ p int_divides q)

INT_DIVIDES_LSUB

|- ∀p q r. p int_divides q ⇒ (p int_divides q − r ⇔ p int_divides r)

INT_DIVIDES_RSUB

|- ∀p q r. p int_divides q ⇒ (p int_divides r − q ⇔ p int_divides r)

INT_EXP

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

INT_EXP_EQ0

|- ∀p n. (p ** n = 0) ⇔ (p = 0) ∧ n ≠ 0

INT_MUL_SIGN_CASES

|- ∀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_EXP_NEG

|- ∀n m. (EVEN n ⇒ (-&m ** n = &(m ** n))) ∧ (ODD n ⇒ (-&m ** n = -&(m ** n)))

INT_EXP_ADD_EXPONENTS

|- ∀n m p. p ** n * p ** m = p ** (n + m)

INT_EXP_MULTIPLY_EXPONENTS

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

INT_EXP_MOD

|- ∀m n p. n ≤ m ∧ p ≠ 0 ⇒ (p ** m % p ** n = 0)

INT_EXP_SUBTRACT_EXPONENTS

|- ∀m n p. n ≤ m ∧ p ≠ 0 ⇒ (p ** m / p ** n = p ** (m − n))

INT_MIN_LT

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

INT_MAX_LT

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

INT_MIN_NUM

|- ∀m n. int_min (&m) (&n) = &MIN m n

INT_MAX_NUM

|- ∀m n. int_max (&m) (&n) = &MAX m n

INT_LT_MONO

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

INT_LE_MONO

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

INFINITE_INT_UNIV

|- INFINITE 𝕌(:int)

INT_ADD_CALCULATE

|- ∀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_REDUCE

|- ∀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_SUB_CALCULATE

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

INT_SUB_REDUCE

|- ∀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_MUL_CALCULATE

|- (∀m n. &m * &n = &(m * n)) ∧ (∀x y. -x * y = -(x * y)) ∧
   (∀x y. x * -y = -(x * y)) ∧ ∀x. - -x = x

INT_MUL_REDUCE

|- ∀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_DIV_CALCULATE

|- (∀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_REDUCE

|- ∀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_QUOT_CALCULATE

|- (∀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_REDUCE

|- ∀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_MOD_CALCULATE

|- (∀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_REDUCE

|- ∀m n.
     (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))) ∧
     (x % &NUMERAL (BIT1 n) = x − x / &NUMERAL (BIT1 n) * &NUMERAL (BIT1 n)) ∧
     (x % &NUMERAL (BIT2 n) = x − x / &NUMERAL (BIT2 n) * &NUMERAL (BIT2 n))

INT_REM_CALCULATE

|- (∀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_REDUCE

|- ∀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_EXP_CALCULATE

|- ∀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_REDUCE

|- ∀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_LT_REDUCE

|- ∀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_LE_CALCULATE

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

INT_LE_REDUCE

|- ∀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_GT_CALCULATE

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

INT_GT_REDUCE

|- ∀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_GE_CALCULATE

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

INT_GE_REDUCE

|- ∀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_EQ_CALCULATE

|- (∀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_REDUCE

|- ∀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_DIVIDES_REDUCE

|- ∀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))