Theory: integer

Parents

• pair
• numeral

Types

• int(Arity = 0)

Constants

• int_0  :int
• int_1  :int
• tint_add  :num # num -> num # num -> num # num
• int_of_num  :num -> int
• tint_neg  :num # num -> num # num
• tint_eq  :num # num -> num # num -> bool
• tint_mul  :num # num -> num # num -> num # num
• tint_lt  :num # num -> num # num -> bool
• int_add  :int -> int -> int
• int_div  :int -> int -> int
• dest_int  :int -> num # num -> bool
• int_exp  :int -> num -> int
• int_max  :int -> int -> int
• int_neg  :int -> int
• int_min  :int -> int -> int
• tint_0  :num # num
• tint_1  :num # num
• int_mod  :int -> int -> int
• int_mul  :int -> int -> int
• int_sub  :int -> int -> int
• int_ge  :int -> int -> bool
• int_gt  :int -> int -> bool
• int_le  :int -> int -> bool
• int_lt  :int -> int -> bool
• ABS  :int -> int
• mk_int  :(num # num -> bool) -> int
• int_divides  :int -> int -> bool
• Num  :int -> num

Definitions

INT_ABS

|- !n. ABS n = (if n < 0 then ~n else n)

INT_DIVIDES

|- !p q. p int_divides q = ?m. m * p = q

int_ge

|- !x y. x >= y = y <= x

int_gt

|- !x y. x > y = y < x

INT_MAX

|- !x y. int_max x y = (if x < y then y else x)

INT_MIN

|- !x y. int_min x y = (if x < y then x else y)

int_neg

|- !T1. ~T1 = mk_int ($tint_eq (tint_neg ($@ (dest_int T1))))

int_TY_DEF

|- ?rep. TYPE_DEFINITION (\c. ?x. c = $tint_eq x) rep

int_tybij

|- (!a. mk_int (dest_int a) = a) /\
   !r. (\c. ?x. c = $tint_eq x) r = (dest_int (mk_int r) = r)

Num

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

tint_0

|- tint_0 = (1,1)

tint_1

|- tint_1 = (1 + 1,1)

tint_add

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

tint_eq

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

tint_lt

|- !x1 y1 x2 y2. (x1,y1) tint_lt (x2,y2) = x1 + y2 < x2 + y1

tint_mul

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

tint_neg

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

Theorems

DEST_MK_EQCLASS

|- !v. dest_int (mk_int ($tint_eq v)) = $tint_eq v

EQ_ADDL

|- !x y. (x = x + y) = (y = 0)

EQ_LADD

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

INT

|- !n. & (SUC n) = & n + 1

INT_0

|- int_0 = 0

INT_1

|- int_1 = 1

INT_10

|- ~(int_1 = int_0)

INT_ABS_ABS

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

INT_ABS_DIV

|- !p q. ~(q = 0) ==> ABS (p / q * q) <= ABS p

INT_ABS_EQ0

|- !p. (ABS p = 0) = (p = 0)

INT_ABS_EQ_ID

|- !p. (ABS p = p) = 0 <= p

INT_ABS_MOD_LT

|- !p q. ~(q = 0) ==> ABS (p % q) < ABS q

INT_ABS_MUL

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

INT_ABS_NEG

|- !p. ABS ~p = ABS p

INT_ABS_NUM

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

INT_ABS_POS

|- !p. 0 <= ABS p

INT_ADD

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

INT_ADD2_SUB2

|- !a b c d. a + b - (c + d) = a - c + (b - d)

INT_ADD_ASSOC

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

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_COMM

|- !y x. x + y = y + x

INT_ADD_LID

|- !x. 0 + x = x

INT_ADD_LID_UNIQ

|- !x y. (x + y = y) = (x = 0)

INT_ADD_LINV

|- !x. ~x + x = 0

INT_ADD_REDUCE

|- !p n m.
     (0 + p = p) /\ (p + 0 = p) /\ (~0 = 0) /\ (~~p = p) /\
     (& (NUMERAL n) + & (NUMERAL m) = & (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 (iZ (n + m))))

INT_ADD_RID

|- !x. x + 0 = x

INT_ADD_RID_UNIQ

|- !x y. (x + y = x) = (y = 0)

INT_ADD_RINV

|- !x. x + ~x = 0

INT_ADD_SUB

|- !x y. x + y - x = y

INT_ADD_SUB2

|- !x y. x - (x + y) = ~y

INT_ADD_SYM

|- !y x. x + y = y + x

INT_DECOMPOSE

|- !i. ?m n. i = mk_int ($tint_eq (m,n))

INT_DIFFSQ

|- !x y. (x + y) * (x - y) = x * x - y * y

INT_DISCRETE

|- !x y. ~(x < y /\ y < x + 1)

INT_DIV

|- !n m. ~(m = 0) ==> (& n / & m = & (n DIV m))

INT_DIV_1

|- !p. p / 1 = p

INT_DIV_CALCULATE

|- (!n m. ~(m = 0) ==> (& n / & m = & (n DIV m))) /\
   (!p q. ~(q = 0) ==> (~p / q = ~(p / q)) /\ (p / ~q = ~p / q)) /\
   (!m n. (& m = & n) = (m = n)) /\ (!x. (~x = 0) = (x = 0)) /\ !x. ~~x = x

INT_DIV_ID

|- !p. ~(p = 0) ==> (p / p = 1)

INT_DIV_MUL_ID

|- !p q. ~(q = 0) /\ (p % q = 0) ==> (p / q * q = p)

INT_DIV_NEG

|- !p q. ~(q = 0) ==> (~p / q = ~(p / q)) /\ (p / ~q = ~p / q)

INT_DIV_REDUCE

|- !m n.
     (0 / & (NUMERAL (NUMERAL_BIT1 n)) = 0) /\
     (0 / & (NUMERAL (NUMERAL_BIT2 n)) = 0) /\
     (& (NUMERAL m) / & (NUMERAL (NUMERAL_BIT1 n)) =
      & (NUMERAL m DIV NUMERAL (NUMERAL_BIT1 n))) /\
     (& (NUMERAL m) / & (NUMERAL (NUMERAL_BIT2 n)) =
      & (NUMERAL m DIV NUMERAL (NUMERAL_BIT2 n))) /\
     (~& (NUMERAL m) / & (NUMERAL (NUMERAL_BIT1 n)) =
      ~& (NUMERAL m DIV NUMERAL (NUMERAL_BIT1 n))) /\
     (~& (NUMERAL m) / & (NUMERAL (NUMERAL_BIT2 n)) =
      ~& (NUMERAL m DIV NUMERAL (NUMERAL_BIT2 n))) /\
     (& (NUMERAL m) / ~& (NUMERAL (NUMERAL_BIT1 n)) =
      ~& (NUMERAL m DIV NUMERAL (NUMERAL_BIT1 n))) /\
     (& (NUMERAL m) / ~& (NUMERAL (NUMERAL_BIT2 n)) =
      ~& (NUMERAL m DIV NUMERAL (NUMERAL_BIT2 n))) /\
     (~& (NUMERAL m) / ~& (NUMERAL (NUMERAL_BIT1 n)) =
      & (NUMERAL m DIV NUMERAL (NUMERAL_BIT1 n))) /\
     (~& (NUMERAL m) / ~& (NUMERAL (NUMERAL_BIT2 n)) =
      & (NUMERAL m DIV NUMERAL (NUMERAL_BIT2 n)))

INT_DIV_UNIQUE

|- !p q k.
     ABS (k * q) <= ABS p /\ (?r. (p = k * q + r) /\ ABS r < ABS q) ==>
     (p / q = k)

INT_DIVIDES_0

|- (!x. x int_divides 0) /\ !x. 0 int_divides x = (x = 0)

INT_DIVIDES_1

|- !x. 1 int_divides x

INT_DIVIDES_LADD

|- !p q r. p int_divides q ==> (p int_divides q + r = p int_divides r)

INT_DIVIDES_LMUL

|- !p q r. p int_divides q ==> p int_divides q * r

INT_DIVIDES_LSUB

|- !p q r. p int_divides q ==> (p int_divides q - r = p int_divides r)

INT_DIVIDES_MOD0

|- !p q. p int_divides q = (q % p = 0) /\ ~(p = 0) \/ (p = 0) /\ (q = 0)

INT_DIVIDES_MUL

|- !p q. p int_divides p * q /\ p int_divides q * p

INT_DIVIDES_NEG

|- !p q.
     (p int_divides ~q = p int_divides q) /\
     (~p int_divides q = p int_divides q)

INT_DIVIDES_RADD

|- !p q r. p int_divides q ==> (p int_divides r + q = p int_divides r)

INT_DIVIDES_REDUCE

|- !n m p.
     (0 int_divides 0 = T) /\
     (0 int_divides & (NUMERAL (NUMERAL_BIT1 n)) = F) /\
     (0 int_divides & (NUMERAL (NUMERAL_BIT2 n)) = F) /\
     (p int_divides 0 = T) /\
     (& (NUMERAL (NUMERAL_BIT1 n)) int_divides & (NUMERAL m) =
      (NUMERAL m MOD NUMERAL (NUMERAL_BIT1 n) = 0)) /\
     (& (NUMERAL (NUMERAL_BIT2 n)) int_divides & (NUMERAL m) =
      (NUMERAL m MOD NUMERAL (NUMERAL_BIT2 n) = 0)) /\
     (& (NUMERAL (NUMERAL_BIT1 n)) int_divides ~& (NUMERAL m) =
      (NUMERAL m MOD NUMERAL (NUMERAL_BIT1 n) = 0)) /\
     (& (NUMERAL (NUMERAL_BIT2 n)) int_divides ~& (NUMERAL m) =
      (NUMERAL m MOD NUMERAL (NUMERAL_BIT2 n) = 0)) /\
     (~& (NUMERAL (NUMERAL_BIT1 n)) int_divides & (NUMERAL m) =
      (NUMERAL m MOD NUMERAL (NUMERAL_BIT1 n) = 0)) /\
     (~& (NUMERAL (NUMERAL_BIT2 n)) int_divides & (NUMERAL m) =
      (NUMERAL m MOD NUMERAL (NUMERAL_BIT2 n) = 0)) /\
     (~& (NUMERAL (NUMERAL_BIT1 n)) int_divides ~& (NUMERAL m) =
      (NUMERAL m MOD NUMERAL (NUMERAL_BIT1 n) = 0)) /\
     (~& (NUMERAL (NUMERAL_BIT2 n)) int_divides ~& (NUMERAL m) =
      (NUMERAL m MOD NUMERAL (NUMERAL_BIT2 n) = 0))

INT_DIVIDES_REFL

|- !x. x int_divides x

INT_DIVIDES_RMUL

|- !p q r. p int_divides q ==> p int_divides r * q

INT_DIVIDES_RSUB

|- !p q r. p int_divides q ==> (p int_divides r - q = p int_divides r)

INT_DIVIDES_TRANS

|- !x y z. x int_divides y /\ y int_divides z ==> x int_divides z

INT_DIVISION

|- !p. ~(p = 0) ==> !q. q = q / p * p + q % p

INT_DOUBLE

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

INT_ENTIRE

|- !x y. (x * y = 0) = (x = 0) \/ (y = 0)

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_IMP_LE

|- !x y. (x = y) ==> x <= y

INT_EQ_LADD

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

INT_EQ_LMUL

|- !x y z. (x * y = x * z) = (x = 0) \/ (y = z)

INT_EQ_LMUL2

|- !x y z. ~(x = 0) ==> ((y = z) = (x * y = x * z))

INT_EQ_LMUL_IMP

|- !x y z. ~(x = 0) /\ (x * y = x * z) ==> (y = z)

INT_EQ_NEG

|- !x y. (~x = ~y) = (x = y)

INT_EQ_RADD

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

INT_EQ_REDUCE

|- !n m.
     ((0 = 0) = T) /\ ((0 = & (NUMERAL (NUMERAL_BIT1 n))) = F) /\
     ((0 = & (NUMERAL (NUMERAL_BIT2 n))) = F) /\
     ((0 = ~& (NUMERAL (NUMERAL_BIT1 n))) = F) /\
     ((0 = ~& (NUMERAL (NUMERAL_BIT2 n))) = F) /\
     ((& (NUMERAL (NUMERAL_BIT1 n)) = 0) = F) /\
     ((& (NUMERAL (NUMERAL_BIT2 n)) = 0) = F) /\
     ((~& (NUMERAL (NUMERAL_BIT1 n)) = 0) = F) /\
     ((~& (NUMERAL (NUMERAL_BIT2 n)) = 0) = F) /\
     ((& (NUMERAL n) = & (NUMERAL m)) = (n = m)) /\
     ((& (NUMERAL (NUMERAL_BIT1 n)) = ~& (NUMERAL m)) = F) /\
     ((& (NUMERAL (NUMERAL_BIT2 n)) = ~& (NUMERAL m)) = F) /\
     ((~& (NUMERAL (NUMERAL_BIT1 n)) = & (NUMERAL m)) = F) /\
     ((~& (NUMERAL (NUMERAL_BIT2 n)) = & (NUMERAL m)) = F) /\
     ((~& (NUMERAL n) = ~& (NUMERAL m)) = (n = m))

INT_EQ_RMUL

|- !x y z. (x * z = y * z) = (z = 0) \/ (x = y)

INT_EQ_RMUL_IMP

|- !x y z. ~(z = 0) /\ (x * z = y * z) ==> (x = y)

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_EXP

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

INT_EXP_ADD_EXPONENTS

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

INT_EXP_CALCULATE

|- !p n m.
     (p ** 0 = 1) /\ (& n ** m = & (n ** m)) /\
     (~& n ** NUMERAL (NUMERAL_BIT1 m) =
      ~& (NUMERAL (n ** NUMERAL (NUMERAL_BIT1 m)))) /\
     (~& n ** NUMERAL (NUMERAL_BIT2 m) =
      & (NUMERAL (n ** NUMERAL (NUMERAL_BIT2 m))))

INT_EXP_EQ0

|- !p n. (p ** n = 0) = (p = 0) /\ ~(n = 0)

INT_EXP_MOD

|- !m n p. n <= m /\ ~(p = 0) ==> (p ** m % p ** n = 0)

INT_EXP_MULTIPLY_EXPONENTS

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

INT_EXP_NEG

|- !n m.
     (EVEN n ==> (~& m ** n = & (m ** n))) /\
     (ODD n ==> (~& m ** n = ~& (m ** n)))

INT_EXP_REDUCE

|- !n m p.
     (p ** 0 = 1) /\ (& (NUMERAL n) ** m = & (n ** m)) /\
     (~& (NUMERAL n) ** NUMERAL (NUMERAL_BIT1 m) =
      ~& (NUMERAL (n ** NUMERAL_BIT1 m))) /\
     (~& (NUMERAL n) ** NUMERAL (NUMERAL_BIT2 m) =
      & (NUMERAL (n ** NUMERAL_BIT2 m)))

INT_EXP_SUBTRACT_EXPONENTS

|- !m n p. n <= m /\ ~(p = 0) ==> (p ** m / p ** n = p ** (m - n))

INT_GE_CALCULATE

|- !x y. x >= y = y <= x

INT_GE_REDUCE

|- !n m.
     (0 >= 0 = T) /\ (& (NUMERAL n) >= 0 = T) /\
     (~& (NUMERAL (NUMERAL_BIT1 n)) >= 0 = F) /\
     (~& (NUMERAL (NUMERAL_BIT2 n)) >= 0 = F) /\
     (0 >= & (NUMERAL (NUMERAL_BIT1 n)) = F) /\
     (0 >= & (NUMERAL (NUMERAL_BIT2 n)) = F) /\
     (0 >= ~& (NUMERAL (NUMERAL_BIT1 n)) = T) /\
     (0 >= ~& (NUMERAL (NUMERAL_BIT2 n)) = T) /\
     (& (NUMERAL m) >= & (NUMERAL n) = n <= m) /\
     (~& (NUMERAL (NUMERAL_BIT1 m)) >= & (NUMERAL n) = F) /\
     (~& (NUMERAL (NUMERAL_BIT2 m)) >= & (NUMERAL n) = F) /\
     (& (NUMERAL m) >= ~& (NUMERAL n) = T) /\
     (~& (NUMERAL m) >= ~& (NUMERAL n) = m <= n)

INT_GT_CALCULATE

|- !x y. x > y = y < x

INT_GT_REDUCE

|- !n m.
     (& (NUMERAL (NUMERAL_BIT1 n)) > 0 = T) /\
     (& (NUMERAL (NUMERAL_BIT2 n)) > 0 = T) /\ (0 > 0 = F) /\
     (~& (NUMERAL n) > 0 = F) /\ (0 > & (NUMERAL n) = F) /\
     (0 > ~& (NUMERAL (NUMERAL_BIT1 n)) = T) /\
     (0 > ~& (NUMERAL (NUMERAL_BIT2 n)) = T) /\
     (& (NUMERAL m) > & (NUMERAL n) = n < m) /\
     (& (NUMERAL m) > ~& (NUMERAL (NUMERAL_BIT1 n)) = T) /\
     (& (NUMERAL m) > ~& (NUMERAL (NUMERAL_BIT2 n)) = T) /\
     (~& (NUMERAL m) > & (NUMERAL n) = F) /\
     (~& (NUMERAL m) > ~& (NUMERAL n) = m < n)

INT_INJ

|- !m n. (& m = & n) = (m = n)

INT_LDISTRIB

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

INT_LE

|- !m n. & m <= & n = m <= n

INT_LE_01

|- 0 <= 1

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_LE_ADDL

|- !x y. y <= x + y = 0 <= x

INT_LE_ADDR

|- !x y. x <= x + y = 0 <= y

INT_LE_ANTISYM

|- !x y. x <= y /\ y <= x = (x = y)

INT_LE_CALCULATE

|- !x y. x <= y = x < y \/ (x = y)

INT_LE_DOUBLE

|- !x. 0 <= x + x = 0 <= x

INT_LE_LADD

|- !x y z. x + y <= x + z = y <= z

INT_LE_LT

|- !x y. x <= y = x < y \/ (x = y)

INT_LE_MUL

|- !x y. 0 <= x /\ 0 <= y ==> 0 <= x * y

INT_LE_NEG

|- !x y. ~x <= ~y = y <= x

INT_LE_NEGL

|- !x. ~x <= x = 0 <= x

INT_LE_NEGR

|- !x. x <= ~x = x <= 0

INT_LE_NEGTOTAL

|- !x. 0 <= x \/ 0 <= ~x

INT_LE_RADD

|- !x y z. x + z <= y + z = x <= y

INT_LE_REDUCE

|- !n m.
     (0 <= 0 = T) /\ (0 <= & (NUMERAL n) = T) /\
     (0 <= ~& (NUMERAL (NUMERAL_BIT1 n)) = F) /\
     (0 <= ~& (NUMERAL (NUMERAL_BIT2 n)) = F) /\
     (& (NUMERAL (NUMERAL_BIT1 n)) <= 0 = F) /\
     (& (NUMERAL (NUMERAL_BIT2 n)) <= 0 = F) /\
     (~& (NUMERAL (NUMERAL_BIT1 n)) <= 0 = T) /\
     (~& (NUMERAL (NUMERAL_BIT2 n)) <= 0 = T) /\
     (& (NUMERAL n) <= & (NUMERAL m) = n <= m) /\
     (& (NUMERAL n) <= ~& (NUMERAL (NUMERAL_BIT1 m)) = F) /\
     (& (NUMERAL n) <= ~& (NUMERAL (NUMERAL_BIT2 m)) = F) /\
     (~& (NUMERAL n) <= & (NUMERAL m) = T) /\
     (~& (NUMERAL n) <= ~& (NUMERAL m) = m <= n)

INT_LE_REFL

|- !x. x <= x

INT_LE_SQUARE

|- !x. 0 <= x * x

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_LE_TOTAL

|- !x y. x <= y \/ y <= x

INT_LE_TRANS

|- !x y z. x <= y /\ y <= z ==> x <= z

INT_LET_ADD

|- !x y. 0 <= x /\ 0 < y ==> 0 < x + y

INT_LET_ADD2

|- !w x y z. w <= x /\ y < z ==> w + y < x + z

INT_LET_ANTISYM

|- !x y. ~(x < y /\ y <= x)

INT_LET_TOTAL

|- !x y. x <= y \/ y < x

INT_LET_TRANS

|- !x y z. x <= y /\ y < z ==> x < z

INT_LNEG_UNIQ

|- !x y. (x + y = 0) = (x = ~y)

INT_LT

|- !m n. & m < & n = m < n

INT_LT_01

|- 0 < 1

INT_LT_ADD

|- !x y. 0 < x /\ 0 < y ==> 0 < x + y

INT_LT_ADD1

|- !x y. x <= y ==> x < y + 1

INT_LT_ADD2

|- !w x y z. w < x /\ y < z ==> w + y < x + z

INT_LT_ADD_SUB

|- !x y z. x + y < z = x < z - y

INT_LT_ADDL

|- !x y. y < x + y = 0 < x

INT_LT_ADDNEG

|- !x y z. y < x + ~z = y + z < x

INT_LT_ADDNEG2

|- !x y z. x + ~y < z = x < z + y

INT_LT_ADDR

|- !x y. x < x + y = 0 < y

INT_LT_ANTISYM

|- !x y. ~(x < y /\ y < x)

INT_LT_CALCULATE

|- !n m.
     (& n < & m = n < m) /\ (~& n < ~& m = m < n) /\
     (~& n < & m = ~(n = 0) \/ ~(m = 0)) /\ (& n < ~& m = F)

INT_LT_GT

|- !x y. x < y ==> ~(y < x)

INT_LT_IMP_LE

|- !x y. x < y ==> x <= y

INT_LT_IMP_NE

|- !x y. x < y ==> ~(x = y)

INT_LT_LADD

|- !x y z. x + y < x + z = y < z

INT_LT_LADD_IMP

|- !x y z. y < z ==> x + y < x + z

INT_LT_LE

|- !x y. x < y = x <= y /\ ~(x = y)

INT_LT_MUL

|- !x y. int_0 < x /\ int_0 < y ==> int_0 < x * y

INT_LT_MUL2

|- !x1 x2 y1 y2.
     0 <= x1 /\ 0 <= y1 /\ x1 < x2 /\ y1 < y2 ==> x1 * y1 < x2 * y2

INT_LT_NEG

|- !x y. ~x < ~y = y < x

INT_LT_NEGTOTAL

|- !x. (x = 0) \/ 0 < x \/ 0 < ~x

INT_LT_NZ

|- !n. ~(& n = 0) = 0 < & n

INT_LT_RADD

|- !x y z. x + z < y + z = x < y

INT_LT_REDUCE

|- !n m.
     (0 < & (NUMERAL (NUMERAL_BIT1 n)) = T) /\
     (0 < & (NUMERAL (NUMERAL_BIT2 n)) = T) /\ (0 < 0 = F) /\
     (0 < ~& (NUMERAL n) = F) /\ (& (NUMERAL n) < 0 = F) /\
     (~& (NUMERAL (NUMERAL_BIT1 n)) < 0 = T) /\
     (~& (NUMERAL (NUMERAL_BIT2 n)) < 0 = T) /\
     (& (NUMERAL n) < & (NUMERAL m) = n < m) /\
     (~& (NUMERAL (NUMERAL_BIT1 n)) < & (NUMERAL m) = T) /\
     (~& (NUMERAL (NUMERAL_BIT2 n)) < & (NUMERAL m) = T) /\
     (& (NUMERAL n) < ~& (NUMERAL m) = F) /\
     (~& (NUMERAL n) < ~& (NUMERAL m) = m < n)

INT_LT_REFL

|- !x. ~(x < x)

INT_LT_SUB_LADD

|- !x y z. x < y - z = x + z < y

INT_LT_SUB_RADD

|- !x y z. x - y < z = x < z + y

INT_LT_TOTAL

|- !x y. (x = y) \/ x < y \/ y < x

INT_LT_TRANS

|- !x y z. x < y /\ y < z ==> x < z

INT_LTE_ADD

|- !x y. 0 < x /\ 0 <= y ==> 0 < x + y

INT_LTE_ADD2

|- !w x y z. w < x /\ y <= z ==> w + y < x + z

INT_LTE_ANTSYM

|- !x y. ~(x <= y /\ y < x)

INT_LTE_TOTAL

|- !x y. x < y \/ y <= x

INT_LTE_TRANS

|- !x y z. x < y /\ y <= z ==> x < z

INT_MAX_LT

|- !x y z. int_max x y < z ==> x < z /\ y < z

INT_MIN_LT

|- !x y z. x < int_min y z ==> x < y /\ x < z

INT_MOD

|- !n m. ~(m = 0) ==> (& n % & m = & (n MOD m))

INT_MOD0

|- !p. ~(p = 0) ==> (0 % p = 0)

INT_MOD_CALCULATE

|- (!n m. ~(m = 0) ==> (& n % & m = & (n MOD m))) /\
   (!p q. ~(q = 0) ==> (~p % q = ~(p % q)) /\ (p % ~q = p % q)) /\
   (!x. ~~x = x) /\ (!m n. (& m = & n) = (m = n)) /\ !x. (~x = 0) = (x = 0)

INT_MOD_COMMON_FACTOR

|- !p. ~(p = 0) ==> !q. (q * p) % p = 0

INT_MOD_EQ0

|- !q. ~(q = 0) ==> !p. (p % q = 0) = ?k. p = k * q

INT_MOD_ID

|- !p. ~(p = 0) ==> (p % p = 0)

INT_MOD_NEG

|- !p q. ~(q = 0) ==> (~p % q = ~(p % q)) /\ (p % ~q = p % q)

INT_MOD_REDUCE

|- !m n.
     (0 % & (NUMERAL (NUMERAL_BIT1 n)) = 0) /\
     (0 % & (NUMERAL (NUMERAL_BIT2 n)) = 0) /\
     (& (NUMERAL m) % & (NUMERAL (NUMERAL_BIT1 n)) =
      & (NUMERAL m MOD NUMERAL (NUMERAL_BIT1 n))) /\
     (& (NUMERAL m) % & (NUMERAL (NUMERAL_BIT2 n)) =
      & (NUMERAL m MOD NUMERAL (NUMERAL_BIT2 n))) /\
     (~& (NUMERAL m) % & (NUMERAL (NUMERAL_BIT1 n)) =
      ~& (NUMERAL m MOD NUMERAL (NUMERAL_BIT1 n))) /\
     (~& (NUMERAL m) % & (NUMERAL (NUMERAL_BIT2 n)) =
      ~& (NUMERAL m MOD NUMERAL (NUMERAL_BIT2 n))) /\
     (& (NUMERAL m) % ~& (NUMERAL (NUMERAL_BIT1 n)) =
      & (NUMERAL m MOD NUMERAL (NUMERAL_BIT1 n))) /\
     (& (NUMERAL m) % ~& (NUMERAL (NUMERAL_BIT2 n)) =
      & (NUMERAL m MOD NUMERAL (NUMERAL_BIT2 n))) /\
     (~& (NUMERAL m) % ~& (NUMERAL (NUMERAL_BIT1 n)) =
      ~& (NUMERAL m MOD NUMERAL (NUMERAL_BIT1 n))) /\
     (~& (NUMERAL m) % ~& (NUMERAL (NUMERAL_BIT2 n)) =
      ~& (NUMERAL m MOD NUMERAL (NUMERAL_BIT2 n)))

INT_MOD_UNIQUE

|- !p q r.
     ABS r < ABS q /\ (?k. ABS (k * q) <= ABS p /\ (p = k * q + r)) ==>
     (p % q = r)

INT_MUL

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

INT_MUL_ASSOC

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

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_COMM

|- !y x. x * y = y * x

INT_MUL_DIV

|- !p q k. ~(q = 0) /\ (p % q = 0) ==> (k * p / q = k * (p / q))

INT_MUL_LID

|- !x. 1 * x = x

INT_MUL_LZERO

|- !x. 0 * x = 0

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_MUL_RID

|- !x. x * 1 = x

INT_MUL_RZERO

|- !x. x * 0 = 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_MUL_SYM

|- !y x. x * y = y * x

INT_NEG_0

|- ~0 = 0

INT_NEG_ADD

|- !x y. ~(x + y) = ~x + ~y

INT_NEG_EQ

|- !x y. (~x = y) = (x = ~y)

INT_NEG_EQ0

|- !x. (~x = 0) = (x = 0)

INT_NEG_GE0

|- !x. 0 <= ~x = x <= 0

INT_NEG_GT0

|- !x. 0 < ~x = x < 0

INT_NEG_LE0

|- !x. ~x <= 0 = 0 <= x

INT_NEG_LMUL

|- !x y. ~(x * y) = ~x * y

INT_NEG_LT0

|- !x. ~x < 0 = 0 < x

INT_NEG_MINUS1

|- !x. ~x = ~1 * x

INT_NEG_MUL2

|- !x y. ~x * ~y = x * y

INT_NEG_RMUL

|- !x y. ~(x * y) = x * ~y

INT_NEG_SAME_EQ

|- !p. (p = ~p) = (p = 0)

INT_NEG_SUB

|- !x y. ~(x - y) = y - x

INT_NEGNEG

|- !x. ~~x = x

INT_NOT_LE

|- !x y. ~(x <= y) = y < x

INT_NOT_LT

|- !x y. ~(x < y) = y <= x

INT_NUM_CASES

|- !p. (?n. (p = & n) /\ ~(n = 0)) \/ (?n. (p = ~& n) /\ ~(n = 0)) \/ (p = 0)

INT_NZ_IMP_LT

|- !n. ~(n = 0) ==> 0 < & n

INT_OF_NUM

|- !i. (& (Num i) = i) = 0 <= i

INT_POASQ

|- !x. 0 < x * x = ~(x = 0)

INT_POS

|- !n. 0 <= & n

INT_POS_NZ

|- !x. 0 < x ==> ~(x = 0)

INT_RDISTRIB

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

INT_RNEG_UNIQ

|- !x y. (x + y = 0) = (y = ~x)

INT_SUB

|- !n m. m <= n ==> (& n - & m = & (n - m))

INT_SUB_0

|- !x y. (x - y = 0) = (x = y)

INT_SUB_ADD

|- !x y. x - y + y = x

INT_SUB_ADD2

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

INT_SUB_CALCULATE

|- !x y. x - y = x + ~y

INT_SUB_LDISTRIB

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

INT_SUB_LE

|- !x y. 0 <= x - y = y <= x

INT_SUB_LNEG

|- !x y. ~x - y = ~(x + y)

INT_SUB_LT

|- !x y. 0 < x - y = y < x

INT_SUB_LZERO

|- !x. 0 - x = ~x

INT_SUB_NEG2

|- !x y. ~x - ~y = y - x

INT_SUB_RDISTRIB

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

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_SUB_REFL

|- !x. x - x = 0

INT_SUB_RNEG

|- !x y. x - ~y = x + y

INT_SUB_RZERO

|- !x. x - 0 = x

INT_SUB_SUB

|- !x y. x - y - x = ~y

INT_SUB_SUB2

|- !x y. x - (x - y) = y

INT_SUB_TRIANGLE

|- !a b c. a - b + (b - c) = a - c

INT_SUMSQ

|- !x y. (x * x + y * y = 0) = (x = 0) /\ (y = 0)

LT_ADD2

|- !x1 x2 y1 y2. x1 < y1 /\ x2 < y2 ==> x1 + x2 < y1 + y2

LT_ADDL

|- !x y. x < x + y = 0 < y

LT_ADDR

|- !x y. ~(x + y < x)

LT_LADD

|- !x y z. x + y < x + z = y < z

NUM_DECOMPOSE

|- !n. & n = mk_int ($tint_eq (n,0))

NUM_LEMMA

|- !i. 0 <= i ==> ?n. i = mk_int ($tint_eq (n,0))

NUM_NEGINT_EXISTS

|- !i. i <= 0 ==> ?n. i = ~& n

NUM_OF_INT

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

NUM_POSINT

|- !i. 0 <= i ==> ?!n. i = & n

NUM_POSINT_EXISTS

|- !i. 0 <= i ==> ?n. i = & n

REP_EQCLASS

|- !v. $@ ($tint_eq v) tint_eq v

TINT_10

|- ~(tint_1 tint_eq tint_0)

TINT_ADD_ASSOC

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

TINT_ADD_LID

|- !x. tint_0 tint_add x tint_eq x

TINT_ADD_LINV

|- !x. tint_neg x tint_add x tint_eq tint_0

TINT_ADD_SYM

|- !x y. x tint_add y = y tint_add x

TINT_ADD_WELLDEF

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

|- !x1 x2 y. x1 tint_eq x2 ==> x1 tint_add y tint_eq x2 tint_add y

TINT_EQ_AP

|- !p q. (p = q) ==> p tint_eq q

TINT_EQ_EQUIV

|- !p q. p tint_eq q = ($tint_eq p = $tint_eq q)

TINT_EQ_REFL

|- !x. x tint_eq x

TINT_EQ_SYM

|- !x y. x tint_eq y = y tint_eq x

TINT_EQ_TRANS

|- !x y z. x tint_eq y /\ y tint_eq z ==> x tint_eq z

TINT_LDISTRIB

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

TINT_LT_ADD

|- !x y z. y tint_lt z ==> x tint_add y tint_lt x tint_add z

TINT_LT_MUL

|- !x y. tint_0 tint_lt x /\ tint_0 tint_lt y ==> tint_0 tint_lt x tint_mul y

TINT_LT_REFL

|- !x. ~(x tint_lt x)

TINT_LT_TOTAL

|- !x y. x tint_eq y \/ x tint_lt y \/ y tint_lt x

TINT_LT_TRANS

|- !x y z. x tint_lt y /\ y tint_lt z ==> x tint_lt z

TINT_LT_WELLDEF

|- !x1 x2 y1 y2.
     x1 tint_eq x2 /\ y1 tint_eq y2 ==> (x1 tint_lt y1 = x2 tint_lt y2)

TINT_LT_WELLDEFL

|- !x y1 y2. y1 tint_eq y2 ==> (x tint_lt y1 = x tint_lt y2)

TINT_LT_WELLDEFR

|- !x1 x2 y. x1 tint_eq x2 ==> (x1 tint_lt y = x2 tint_lt y)

TINT_MUL_ASSOC

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

TINT_MUL_LID

|- !x. tint_1 tint_mul x tint_eq x

TINT_MUL_SYM

|- !x y. x tint_mul y = y tint_mul x

TINT_MUL_WELLDEF

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

|- !x1 x2 y. x1 tint_eq x2 ==> x1 tint_mul y tint_eq x2 tint_mul y

TINT_NEG_WELLDEF

|- !x1 x2. x1 tint_eq x2 ==> tint_neg x1 tint_eq tint_neg x2