Theory "arithmetic"

Parents prim_rec pair

Signature

Constant	Type
*	:num -> num -> num
+	:num -> num -> num
-	:num -> num -> num
<=	:num reln
>	:num reln
>=	:num reln
ABS_DIFF	:num -> num -> num
BIT1	:num -> num
BIT2	:num -> num
DIV	:num -> num -> num
DIV2	:num -> num
DIVMOD	:num # num # num -> num # num
EVEN	:num -> bool
EXP	:num -> num -> num
FACT	:num -> num
FUNPOW	:(α -> α) -> num -> α -> α
MAX	:num -> num -> num
MIN	:num -> num -> num
MOD	:num -> num -> num
MODEQ	:num -> num reln
NRC	:α reln -> num -> α reln
NUMERAL	:num -> num
ODD	:num -> bool
ZERO	:num
findq	:num # num # num -> num
nat_elim__magic	:num -> num
num_CASE	:num -> α -> (num -> α) -> α

Definitions

ADD

⊢ (∀n. 0 + n = n) ∧ ∀m n. SUC m + n = SUC (m + n)

NUMERAL_DEF

⊢ ∀x. NUMERAL x = x

ALT_ZERO

⊢ ZERO = 0

BIT1

⊢ ∀n. BIT1 n = n + (n + SUC 0)

BIT2

⊢ ∀n. BIT2 n = n + (n + SUC (SUC 0))

nat_elim__magic

⊢ ∀n. &n = n

SUB

⊢ (∀m. 0 − m = 0) ∧ ∀m n. SUC m − n = if m < n then 0 else SUC (m − n)

MULT

⊢ (∀n. 0 * n = 0) ∧ ∀m n. SUC m * n = m * n + n

EXP

⊢ (∀m. m ** 0 = 1) ∧ ∀m n. m ** SUC n = m * m ** n

GREATER_DEF

⊢ ∀m n. m > n ⇔ n < m

LESS_OR_EQ

⊢ ∀m n. m ≤ n ⇔ m < n ∨ m = n

GREATER_OR_EQ

⊢ ∀m n. m ≥ n ⇔ m > n ∨ m = n

EVEN

⊢ (EVEN 0 ⇔ T) ∧ ∀n. EVEN (SUC n) ⇔ ¬EVEN n

ODD

⊢ (ODD 0 ⇔ F) ∧ ∀n. ODD (SUC n) ⇔ ¬ODD n

num_case_def

⊢ (∀v f. num_CASE 0 v f = v) ∧ ∀n v f. num_CASE (SUC n) v f = f n

FUNPOW

⊢ (∀f x. FUNPOW f 0 x = x) ∧ ∀f n x. FUNPOW f (SUC n) x = FUNPOW f n (f x)

NRC

⊢ (∀R x y. NRC R 0 x y ⇔ x = y) ∧
  ∀R n x y. NRC R (SUC n) x y ⇔ ∃z. R x z ∧ NRC R n z y

FACT

⊢ FACT 0 = 1 ∧ ∀n. FACT (SUC n) = SUC n * FACT n

DIVISION

⊢ ∀n. 0 < n ⇒ ∀k. k = k DIV n * n + k MOD n ∧ k MOD n < n

DIV2_def

⊢ ∀n. DIV2 n = n DIV 2

MAX_DEF

⊢ ∀m n. MAX m n = if m < n then n else m

MIN_DEF

⊢ ∀m n. MIN m n = if m < n then m else n

ABS_DIFF_def

⊢ ∀n m. ABS_DIFF n m = if n < m then m − n else n − m

findq_def

⊢ findq =
  WFREC (measure (λ(a,m,n). m − n))
    (λf (a,m,n).
         if n = 0 then a
         else (let d = 2 * n in if m < d then a else f (2 * a,m,d)))

DIVMOD_DEF

⊢ DIVMOD =
  WFREC (measure (FST ∘ SND))
    (λf (a,m,n).
         if n = 0 then (0,0)
         else if m < n then (a,m)
         else (let q = findq (1,m,n) in f (a + q,m − n * q,n)))

MODEQ_DEF

⊢ ∀n m1 m2. MODEQ n m1 m2 ⇔ ∃a b. a * n + m1 = b * n + m2

Theorems

ONE

⊢ 1 = SUC 0

TWO

⊢ 2 = SUC 1

NORM_0

⊢ 0 = 0

num_case_compute

⊢ ∀n. num_CASE n f g = if n = 0 then f else g (PRE n)

SUC_NOT

⊢ ∀n. 0 ≠ SUC n

ADD_0

⊢ ∀m. m + 0 = m

ADD_SUC

⊢ ∀m n. SUC (m + n) = m + SUC n

ADD_CLAUSES

⊢ 0 + m = m ∧ m + 0 = m ∧ SUC m + n = SUC (m + n) ∧ m + SUC n = SUC (m + n)

ADD_SYM

⊢ ∀m n. m + n = n + m

ADD_COMM

⊢ ∀m n. m + n = n + m

ADD_ASSOC

⊢ ∀m n p. m + (n + p) = m + n + p

num_CASES

⊢ ∀m. m = 0 ∨ ∃n. m = SUC n

NOT_ZERO_LT_ZERO

⊢ ∀n. n ≠ 0 ⇔ 0 < n

NOT_LT_ZERO_EQ_ZERO

⊢ ∀n. ¬(0 < n) ⇔ n = 0

LESS_OR_EQ_ALT

⊢ $<= = (λx y. y = SUC x)^*

LESS_ADD

⊢ ∀m n. n < m ⇒ ∃p. p + n = m

transitive_LESS

⊢ transitive $<

LESS_TRANS

⊢ ∀m n p. m < n ∧ n < p ⇒ m < p

LESS_ANTISYM

⊢ ∀m n. ¬(m < n ∧ n < m)

LESS_MONO_REV

⊢ ∀m n. SUC m < SUC n ⇒ m < n

LESS_MONO_EQ

⊢ ∀m n. SUC m < SUC n ⇔ m < n

LESS_EQ_MONO

⊢ ∀n m. SUC n ≤ SUC m ⇔ n ≤ m

LESS_LESS_SUC

⊢ ∀m n. ¬(m < n ∧ n < SUC m)

transitive_measure

⊢ ∀f. transitive (measure f)

LESS_EQ

⊢ ∀m n. m < n ⇔ SUC m ≤ n

LESS_OR

⊢ ∀m n. m < n ⇒ SUC m ≤ n

OR_LESS

⊢ ∀m n. SUC m ≤ n ⇒ m < n

LESS_EQ_IFF_LESS_SUC

⊢ ∀n m. n ≤ m ⇔ n < SUC m

LESS_EQ_IMP_LESS_SUC

⊢ ∀n m. n ≤ m ⇒ n < SUC m

ZERO_LESS_EQ

⊢ ∀n. 0 ≤ n

LESS_SUC_EQ_COR

⊢ ∀m n. m < n ∧ SUC m ≠ n ⇒ SUC m < n

LESS_NOT_SUC

⊢ ∀m n. m < n ∧ n ≠ SUC m ⇒ SUC m < n

LESS_0_CASES

⊢ ∀m. 0 = m ∨ 0 < m

LESS_CASES_IMP

⊢ ∀m n. ¬(m < n) ∧ m ≠ n ⇒ n < m

LESS_CASES

⊢ ∀m n. m < n ∨ n ≤ m

ADD_INV_0

⊢ ∀m n. m + n = m ⇒ n = 0

LESS_EQ_ADD

⊢ ∀m n. m ≤ m + n

LESS_EQ_ADD_EXISTS

⊢ ∀m n. n ≤ m ⇒ ∃p. p + n = m

LESS_STRONG_ADD

⊢ ∀m n. n < m ⇒ ∃p. SUC p + n = m

LESS_EQ_SUC_REFL

⊢ ∀m. m ≤ SUC m

LESS_ADD_NONZERO

⊢ ∀m n. n ≠ 0 ⇒ m < m + n

NOT_SUC_LESS_EQ_0

⊢ ∀n. ¬(SUC n ≤ 0)

NOT_LESS

⊢ ∀m n. ¬(m < n) ⇔ n ≤ m

NOT_LESS_EQUAL

⊢ ∀m n. ¬(m ≤ n) ⇔ n < m

LESS_EQ_ANTISYM

⊢ ∀m n. ¬(m < n ∧ n ≤ m)

LESS_EQ_0

⊢ ∀n. n ≤ 0 ⇔ n = 0

SUB_0

⊢ ∀m. 0 − m = 0 ∧ m − 0 = m

SUB_MONO_EQ

⊢ ∀n m. SUC n − SUC m = n − m

SUB_EQ_0

⊢ ∀m n. m − n = 0 ⇔ m ≤ n

ADD1

⊢ ∀m. SUC m = m + 1

SUC_SUB1

⊢ ∀m. SUC m − 1 = m

PRE_SUB1

⊢ ∀m. PRE m = m − 1

MULT_0

⊢ ∀m. m * 0 = 0

MULT_SUC

⊢ ∀m n. m * SUC n = m + m * n

MULT_LEFT_1

⊢ ∀m. 1 * m = m

MULT_RIGHT_1

⊢ ∀m. m * 1 = m

MULT_CLAUSES

⊢ ∀m n.
      0 * m = 0 ∧ m * 0 = 0 ∧ 1 * m = m ∧ m * 1 = m ∧ SUC m * n = m * n + n ∧
      m * SUC n = m + m * n

MULT_SYM

⊢ ∀m n. m * n = n * m

MULT_COMM

⊢ ∀m n. m * n = n * m

RIGHT_ADD_DISTRIB

⊢ ∀m n p. (m + n) * p = m * p + n * p

LEFT_ADD_DISTRIB

⊢ ∀m n p. p * (m + n) = p * m + p * n

MULT_ASSOC

⊢ ∀m n p. m * (n * p) = m * n * p

SUB_ADD

⊢ ∀m n. n ≤ m ⇒ m − n + n = m

PRE_SUB

⊢ ∀m n. PRE (m − n) = PRE m − n

ADD_EQ_0

⊢ ∀m n. m + n = 0 ⇔ m = 0 ∧ n = 0

ADD_EQ_1

⊢ ∀m n. m + n = 1 ⇔ m = 1 ∧ n = 0 ∨ m = 0 ∧ n = 1

ADD_INV_0_EQ

⊢ ∀m n. m + n = m ⇔ n = 0

PRE_SUC_EQ

⊢ ∀m n. 0 < n ⇒ (m = PRE n ⇔ SUC m = n)

INV_PRE_EQ

⊢ ∀m n. 0 < m ∧ 0 < n ⇒ (PRE m = PRE n ⇔ m = n)

LESS_SUC_NOT

⊢ ∀m n. m < n ⇒ ¬(n < SUC m)

ADD_EQ_SUB

⊢ ∀m n p. n ≤ p ⇒ (m + n = p ⇔ m = p − n)

LESS_MONO_ADD

⊢ ∀m n p. m < n ⇒ m + p < n + p

LESS_MONO_ADD_INV

⊢ ∀m n p. m + p < n + p ⇒ m < n

LESS_MONO_ADD_EQ

⊢ ∀m n p. m + p < n + p ⇔ m < n

LT_ADD_RCANCEL

⊢ ∀m n p. m + p < n + p ⇔ m < n

LT_ADD_LCANCEL

⊢ ∀m n p. p + m < p + n ⇔ m < n

EQ_MONO_ADD_EQ

⊢ ∀m n p. m + p = n + p ⇔ m = n

LESS_EQ_MONO_ADD_EQ

⊢ ∀m n p. m + p ≤ n + p ⇔ m ≤ n

LESS_EQ_TRANS

⊢ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

LESS_EQ_LESS_TRANS

⊢ ∀m n p. m ≤ n ∧ n < p ⇒ m < p

LESS_LESS_EQ_TRANS

⊢ ∀m n p. m < n ∧ n ≤ p ⇒ m < p

LESS_EQ_LESS_EQ_MONO

⊢ ∀m n p q. m ≤ p ∧ n ≤ q ⇒ m + n ≤ p + q

LESS_EQ_REFL

⊢ ∀m. m ≤ m

LESS_IMP_LESS_OR_EQ

⊢ ∀m n. m < n ⇒ m ≤ n

LESS_MONO_MULT

⊢ ∀m n p. m ≤ n ⇒ m * p ≤ n * p

LESS_MONO_MULT2

⊢ ∀m n i j. m ≤ i ∧ n ≤ j ⇒ m * n ≤ i * j

RIGHT_SUB_DISTRIB

⊢ ∀m n p. (m − n) * p = m * p − n * p

LEFT_SUB_DISTRIB

⊢ ∀m n p. p * (m − n) = p * m − p * n

LESS_ADD_1

⊢ ∀m n. n < m ⇒ ∃p. m = n + (p + 1)

EXP_ADD

⊢ ∀p q n. n ** (p + q) = n ** p * n ** q

NOT_ODD_EQ_EVEN

⊢ ∀n m. SUC (n + n) ≠ m + m

LESS_EQUAL_ANTISYM

⊢ ∀n m. n ≤ m ∧ m ≤ n ⇒ n = m

LESS_ADD_SUC

⊢ ∀m n. m < m + SUC n

LESS_OR_EQ_ADD

⊢ ∀n m. n < m ∨ ∃p. n = p + m

WOP

⊢ ∀P. (∃n. P n) ⇒ ∃n. P n ∧ ∀m. m < n ⇒ ¬P m

COMPLETE_INDUCTION

⊢ ∀P. (∀n. (∀m. m < n ⇒ P m) ⇒ P n) ⇒ ∀n. P n

FORALL_NUM_THM

⊢ (∀n. P n) ⇔ P 0 ∧ ∀n. P n ⇒ P (SUC n)

SUC_SUB

⊢ ∀a. SUC a − a = 1

SUB_PLUS

⊢ ∀a b c. a − (b + c) = a − b − c

INV_PRE_LESS

⊢ ∀m. 0 < m ⇒ ∀n. PRE m < PRE n ⇔ m < n

INV_PRE_LESS_EQ

⊢ ∀n. 0 < n ⇒ ∀m. PRE m ≤ PRE n ⇔ m ≤ n

PRE_LESS_EQ

⊢ ∀n. m ≤ n ⇒ PRE m ≤ PRE n

SUB_LESS_EQ

⊢ ∀n m. n − m ≤ n

SUB_EQ_EQ_0

⊢ ∀m n. m − n = m ⇔ m = 0 ∨ n = 0

SUB_LESS_0

⊢ ∀n m. m < n ⇔ 0 < n − m

SUB_LESS_OR

⊢ ∀m n. n < m ⇒ n ≤ m − 1

LESS_SUB_ADD_LESS

⊢ ∀n m i. i < n − m ⇒ i + m < n

TIMES2

⊢ ∀n. 2 * n = n + n

LESS_MULT_MONO

⊢ ∀m i n. SUC n * m < SUC n * i ⇔ m < i

MULT_MONO_EQ

⊢ ∀m i n. SUC n * m = SUC n * i ⇔ m = i

MULT_SUC_EQ

⊢ ∀p m n. n * SUC p = m * SUC p ⇔ n = m

MULT_EXP_MONO

⊢ ∀p q n m. n * SUC q ** p = m * SUC q ** p ⇔ n = m

EQ_ADD_LCANCEL

⊢ ∀m n p. m + n = m + p ⇔ n = p

EQ_ADD_RCANCEL

⊢ ∀m n p. m + p = n + p ⇔ m = n

EQ_MULT_LCANCEL

⊢ ∀m n p. m * n = m * p ⇔ m = 0 ∨ n = p

EQ_MULT_RCANCEL

⊢ ∀m n p. n * m = p * m ⇔ m = 0 ∨ n = p

ADD_SUB

⊢ ∀a c. a + c − c = a

LESS_EQ_ADD_SUB

⊢ ∀c b. c ≤ b ⇒ ∀a. a + b − c = a + (b − c)

SUB_EQUAL_0

⊢ ∀c. c − c = 0

LESS_EQ_SUB_LESS

⊢ ∀a b. b ≤ a ⇒ ∀c. a − b < c ⇔ a < b + c

NOT_SUC_LESS_EQ

⊢ ∀n m. ¬(SUC n ≤ m) ⇔ m ≤ n

SUB_SUB

⊢ ∀b c. c ≤ b ⇒ ∀a. a − (b − c) = a + c − b

LESS_IMP_LESS_ADD

⊢ ∀n m. n < m ⇒ ∀p. n < m + p

SUB_LESS_EQ_ADD

⊢ ∀m p. m ≤ p ⇒ ∀n. p − m ≤ n ⇔ p ≤ m + n

SUB_LESS_SUC

⊢ ∀p m. p − m < SUC p

SUB_CANCEL

⊢ ∀p n m. n ≤ p ∧ m ≤ p ⇒ (p − n = p − m ⇔ n = m)

CANCEL_SUB

⊢ ∀p n m. p ≤ n ∧ p ≤ m ⇒ (n − p = m − p ⇔ n = m)

NOT_EXP_0

⊢ ∀m n. SUC n ** m ≠ 0

ZERO_LESS_EXP

⊢ ∀m n. 0 < SUC n ** m

ODD_OR_EVEN

⊢ ∀n. ∃m. n = SUC (SUC 0) * m ∨ n = SUC (SUC 0) * m + 1

LESS_EXP_SUC_MONO

⊢ ∀n m. SUC (SUC m) ** n < SUC (SUC m) ** SUC n

LESS_LESS_CASES

⊢ ∀m n. m = n ∨ m < n ∨ n < m

GREATER_EQ

⊢ ∀n m. n ≥ m ⇔ m ≤ n

LESS_EQ_CASES

⊢ ∀m n. m ≤ n ∨ n ≤ m

LESS_EQUAL_ADD

⊢ ∀m n. m ≤ n ⇒ ∃p. n = m + p

LESS_EQ_EXISTS

⊢ ∀m n. m ≤ n ⇔ ∃p. n = m + p

MULT_EQ_0

⊢ ∀m n. m * n = 0 ⇔ m = 0 ∨ n = 0

MULT_EQ_1

⊢ ∀x y. x * y = 1 ⇔ x = 1 ∧ y = 1

MULT_EQ_ID

⊢ ∀m n. m * n = n ⇔ m = 1 ∨ n = 0

LESS_MULT2

⊢ ∀m n. 0 < m ∧ 0 < n ⇒ 0 < m * n

ZERO_LESS_MULT

⊢ ∀m n. 0 < m * n ⇔ 0 < m ∧ 0 < n

ZERO_LESS_ADD

⊢ ∀m n. 0 < m + n ⇔ 0 < m ∨ 0 < n

FACT_LESS

⊢ ∀n. 0 < FACT n

EVEN_ODD

⊢ ∀n. EVEN n ⇔ ¬ODD n

ODD_EVEN

⊢ ∀n. ODD n ⇔ ¬EVEN n

EVEN_OR_ODD

⊢ ∀n. EVEN n ∨ ODD n

EVEN_AND_ODD

⊢ ∀n. ¬(EVEN n ∧ ODD n)

EVEN_ADD

⊢ ∀m n. EVEN (m + n) ⇔ (EVEN m ⇔ EVEN n)

EVEN_MULT

⊢ ∀m n. EVEN (m * n) ⇔ EVEN m ∨ EVEN n

ODD_ADD

⊢ ∀m n. ODD (m + n) ⇔ (ODD m ⇎ ODD n)

ODD_MULT

⊢ ∀m n. ODD (m * n) ⇔ ODD m ∧ ODD n

EVEN_DOUBLE

⊢ ∀n. EVEN (2 * n)

ODD_DOUBLE

⊢ ∀n. ODD (SUC (2 * n))

EVEN_ODD_EXISTS

⊢ ∀n. (EVEN n ⇒ ∃m. n = 2 * m) ∧ (ODD n ⇒ ∃m. n = SUC (2 * m))

EVEN_EXISTS

⊢ ∀n. EVEN n ⇔ ∃m. n = 2 * m

ODD_EXISTS

⊢ ∀n. ODD n ⇔ ∃m. n = SUC (2 * m)

EVEN_EXP_IFF

⊢ ∀n m. EVEN (m ** n) ⇔ 0 < n ∧ EVEN m

EVEN_EXP

⊢ ∀m n. 0 < n ∧ EVEN m ⇒ EVEN (m ** n)

ODD_EXP_IFF

⊢ ∀n m. ODD (m ** n) ⇔ n = 0 ∨ ODD m

ODD_EXP

⊢ ∀m n. 0 < n ∧ ODD m ⇒ ODD (m ** n)

EQ_LESS_EQ

⊢ ∀m n. m = n ⇔ m ≤ n ∧ n ≤ m

ADD_MONO_LESS_EQ

⊢ ∀m n p. m + n ≤ m + p ⇔ n ≤ p

LE_ADD_LCANCEL

⊢ ∀m n p. m + n ≤ m + p ⇔ n ≤ p

LE_ADD_RCANCEL

⊢ ∀m n p. n + m ≤ p + m ⇔ n ≤ p

NOT_LEQ

⊢ ∀m n. ¬(m ≤ n) ⇔ SUC n ≤ m

NOT_NUM_EQ

⊢ ∀m n. m ≠ n ⇔ SUC m ≤ n ∨ SUC n ≤ m

NOT_GREATER

⊢ ∀m n. ¬(m > n) ⇔ m ≤ n

NOT_GREATER_EQ

⊢ ∀m n. ¬(m ≥ n) ⇔ SUC m ≤ n

SUC_ONE_ADD

⊢ ∀n. SUC n = 1 + n

SUC_ADD_SYM

⊢ ∀m n. SUC (m + n) = SUC n + m

NOT_SUC_ADD_LESS_EQ

⊢ ∀m n. ¬(SUC (m + n) ≤ m)

MULT_LESS_EQ_SUC

⊢ ∀m n p. m ≤ n ⇔ SUC p * m ≤ SUC p * n

LE_MULT_LCANCEL

⊢ ∀m n p. m * n ≤ m * p ⇔ m = 0 ∨ n ≤ p

LE_MULT_RCANCEL

⊢ ∀m n p. m * n ≤ p * n ⇔ n = 0 ∨ m ≤ p

LT_MULT_LCANCEL

⊢ ∀m n p. m * n < m * p ⇔ 0 < m ∧ n < p

LT_MULT_RCANCEL

⊢ ∀m n p. m * n < p * n ⇔ 0 < n ∧ m < p

LT_MULT_CANCEL_LBARE

⊢ (m < m * n ⇔ 0 < m ∧ 1 < n) ∧ (m < n * m ⇔ 0 < m ∧ 1 < n)

LT_MULT_CANCEL_RBARE

⊢ (m * n < m ⇔ 0 < m ∧ n = 0) ∧ (m * n < n ⇔ 0 < n ∧ m = 0)

LE_MULT_CANCEL_LBARE

⊢ (m ≤ m * n ⇔ m = 0 ∨ 0 < n) ∧ (m ≤ n * m ⇔ m = 0 ∨ 0 < n)

LE_MULT_CANCEL_RBARE

⊢ (m * n ≤ m ⇔ m = 0 ∨ n ≤ 1) ∧ (m * n ≤ n ⇔ n = 0 ∨ m ≤ 1)

SUB_LEFT_ADD

⊢ ∀m n p. m + (n − p) = if n ≤ p then m else m + n − p

SUB_RIGHT_ADD

⊢ ∀m n p. m − n + p = if m ≤ n then p else m + p − n

SUB_LEFT_SUB

⊢ ∀m n p. m − (n − p) = if n ≤ p then m else m + p − n

SUB_RIGHT_SUB

⊢ ∀m n p. m − n − p = m − (n + p)

SUB_LEFT_SUC

⊢ ∀m n. SUC (m − n) = if m ≤ n then SUC 0 else SUC m − n

SUB_LEFT_LESS_EQ

⊢ ∀m n p. m ≤ n − p ⇔ m + p ≤ n ∨ m ≤ 0

SUB_RIGHT_LESS_EQ

⊢ ∀m n p. m − n ≤ p ⇔ m ≤ n + p

SUB_LEFT_LESS

⊢ ∀m n p. m < n − p ⇔ m + p < n

SUB_RIGHT_LESS

⊢ ∀m n p. m − n < p ⇔ m < n + p ∧ 0 < p

SUB_LEFT_GREATER_EQ

⊢ ∀m n p. m ≥ n − p ⇔ m + p ≥ n

SUB_RIGHT_GREATER_EQ

⊢ ∀m n p. m − n ≥ p ⇔ m ≥ n + p ∨ 0 ≥ p

SUB_LEFT_GREATER

⊢ ∀m n p. m > n − p ⇔ m + p > n ∧ m > 0

SUB_RIGHT_GREATER

⊢ ∀m n p. m − n > p ⇔ m > n + p

SUB_LEFT_EQ

⊢ ∀m n p. m = n − p ⇔ m + p = n ∨ m ≤ 0 ∧ n ≤ p

SUB_RIGHT_EQ

⊢ ∀m n p. m − n = p ⇔ m = n + p ∨ m ≤ n ∧ p ≤ 0

LE

⊢ (∀n. n ≤ 0 ⇔ n = 0) ∧ ∀m n. m ≤ SUC n ⇔ m = SUC n ∨ m ≤ n

DA

⊢ ∀k n. 0 < n ⇒ ∃r q. k = q * n + r ∧ r < n

MOD_ONE

⊢ ∀k. k MOD SUC 0 = 0

MOD_1

⊢ ∀k. k MOD 1 = 0

DIV_LESS_EQ

⊢ ∀n. 0 < n ⇒ ∀k. k DIV n ≤ k

DIV_UNIQUE

⊢ ∀n k q. (∃r. k = q * n + r ∧ r < n) ⇒ k DIV n = q

MOD_UNIQUE

⊢ ∀n k r. (∃q. k = q * n + r ∧ r < n) ⇒ k MOD n = r

DIV_MULT

⊢ ∀n r. r < n ⇒ ∀q. (q * n + r) DIV n = q

LESS_MOD

⊢ ∀n k. k < n ⇒ k MOD n = k

MOD_EQ_0

⊢ ∀n. 0 < n ⇒ ∀k. (k * n) MOD n = 0

ZERO_MOD

⊢ ∀n. 0 < n ⇒ 0 MOD n = 0

ZERO_DIV

⊢ ∀n. 0 < n ⇒ 0 DIV n = 0

MOD_MULT

⊢ ∀n r. r < n ⇒ ∀q. (q * n + r) MOD n = r

MOD_TIMES

⊢ ∀n. 0 < n ⇒ ∀q r. (q * n + r) MOD n = r MOD n

MOD_TIMES_SUB

⊢ ∀n q r. 0 < n ∧ 0 < q ∧ r ≤ n ⇒ (q * n − r) MOD n = (n − r) MOD n

MOD_PLUS

⊢ ∀n. 0 < n ⇒ ∀j k. (j MOD n + k MOD n) MOD n = (j + k) MOD n

MOD_MOD

⊢ ∀n. 0 < n ⇒ ∀k. k MOD n MOD n = k MOD n

LESS_DIV_EQ_ZERO

⊢ ∀r n. r < n ⇒ r DIV n = 0

MULT_DIV

⊢ ∀n q. 0 < n ⇒ q * n DIV n = q

ADD_DIV_ADD_DIV

⊢ ∀n. 0 < n ⇒ ∀x r. (x * n + r) DIV n = x + r DIV n

ADD_DIV_RWT

⊢ ∀n.
      0 < n ⇒
      ∀m p. m MOD n = 0 ∨ p MOD n = 0 ⇒ (m + p) DIV n = m DIV n + p DIV n

MOD_MULT_MOD

⊢ ∀m n. 0 < n ∧ 0 < m ⇒ ∀x. x MOD (n * m) MOD n = x MOD n

DIV_ONE

⊢ ∀q. q DIV SUC 0 = q

DIV_1

⊢ ∀q. q DIV 1 = q

DIVMOD_ID

⊢ ∀n. 0 < n ⇒ n DIV n = 1 ∧ n MOD n = 0

DIV_DIV_DIV_MULT

⊢ ∀m n. 0 < m ∧ 0 < n ⇒ ∀x. x DIV m DIV n = x DIV (m * n)

SUC_PRE

⊢ 0 < m ⇔ SUC (PRE m) = m

DIV_LESS

⊢ ∀n d. 0 < n ∧ 1 < d ⇒ n DIV d < n

MOD_LESS

⊢ ∀m n. 0 < n ⇒ m MOD n < n

ADD_MODULUS

⊢ (∀n x. 0 < n ⇒ (x + n) MOD n = x MOD n) ∧
  ∀n x. 0 < n ⇒ (n + x) MOD n = x MOD n

ADD_MODULUS_LEFT

⊢ ∀n x. 0 < n ⇒ (x + n) MOD n = x MOD n

ADD_MODULUS_RIGHT

⊢ ∀n x. 0 < n ⇒ (n + x) MOD n = x MOD n

DIV_P

⊢ ∀P p q. 0 < q ⇒ (P (p DIV q) ⇔ ∃k r. p = k * q + r ∧ r < q ∧ P k)

DIV_P_UNIV

⊢ ∀P m n. 0 < n ⇒ (P (m DIV n) ⇔ ∀q r. m = q * n + r ∧ r < n ⇒ P q)

MOD_P

⊢ ∀P p q. 0 < q ⇒ (P (p MOD q) ⇔ ∃k r. p = k * q + r ∧ r < q ∧ P r)

MOD_P_UNIV

⊢ ∀P m n. 0 < n ⇒ (P (m MOD n) ⇔ ∀q r. m = q * n + r ∧ r < n ⇒ P r)

MOD_TIMES2

⊢ ∀n. 0 < n ⇒ ∀j k. (j MOD n * k MOD n) MOD n = (j * k) MOD n

MOD_COMMON_FACTOR

⊢ ∀n p q. 0 < n ∧ 0 < q ⇒ n * p MOD q = (n * p) MOD (n * q)

X_MOD_Y_EQ_X

⊢ ∀x y. 0 < y ⇒ (x MOD y = x ⇔ x < y)

DIV_LE_MONOTONE

⊢ ∀n x y. 0 < n ∧ x ≤ y ⇒ x DIV n ≤ y DIV n

LE_LT1

⊢ ∀x y. x ≤ y ⇔ x < y + 1

X_LE_DIV

⊢ ∀x y z. 0 < z ⇒ (x ≤ y DIV z ⇔ x * z ≤ y)

X_LT_DIV

⊢ ∀x y z. 0 < z ⇒ (x < y DIV z ⇔ (x + 1) * z ≤ y)

DIV_LT_X

⊢ ∀x y z. 0 < z ⇒ (y DIV z < x ⇔ y < x * z)

DIV_LE_X

⊢ ∀x y z. 0 < z ⇒ (y DIV z ≤ x ⇔ y < (x + 1) * z)

DIV_EQ_X

⊢ ∀x y z. 0 < z ⇒ (y DIV z = x ⇔ x * z ≤ y ∧ y < SUC x * z)

DIV_MOD_MOD_DIV

⊢ ∀m n k. 0 < n ∧ 0 < k ⇒ (m DIV n) MOD k = m MOD (n * k) DIV n

MULT_EQ_DIV

⊢ 0 < x ⇒ (x * y = z ⇔ y = z DIV x ∧ z MOD x = 0)

NUMERAL_MULT_EQ_DIV

⊢ (NUMERAL (BIT1 x) * y = NUMERAL z ⇔
   y = NUMERAL z DIV NUMERAL (BIT1 x) ∧ NUMERAL z MOD NUMERAL (BIT1 x) = 0) ∧
  (NUMERAL (BIT2 x) * y = NUMERAL z ⇔
   y = NUMERAL z DIV NUMERAL (BIT2 x) ∧ NUMERAL z MOD NUMERAL (BIT2 x) = 0)

MOD_EQ_0_DIVISOR

⊢ 0 < n ⇒ (k MOD n = 0 ⇔ ∃d. k = d * n)

MOD_SUC

⊢ 0 < y ∧ SUC x ≠ SUC (x DIV y) * y ⇒ SUC x MOD y = SUC (x MOD y)

MOD_SUC_IFF

⊢ 0 < y ⇒ (SUC x MOD y = SUC (x MOD y) ⇔ SUC x ≠ SUC (x DIV y) * y)

ONE_MOD

⊢ 1 < n ⇒ 1 MOD n = 1

ONE_MOD_IFF

⊢ 1 < n ⇔ 0 < n ∧ 1 MOD n = 1

MOD_LESS_EQ

⊢ 0 < y ⇒ x MOD y ≤ x

MOD_LIFT_PLUS

⊢ 0 < n ∧ k < n − x MOD n ⇒ (x + k) MOD n = x MOD n + k

MOD_LIFT_PLUS_IFF

⊢ 0 < n ⇒ ((x + k) MOD n = x MOD n + k ⇔ k < n − x MOD n)

num_case_cong

⊢ ∀M M' v f.
      M = M' ∧ (M' = 0 ⇒ v = v') ∧ (∀n. M' = SUC n ⇒ f n = f' n) ⇒
      num_CASE M v f = num_CASE M' v' f'

SUC_ELIM_THM

⊢ ∀P. (∀n. P (SUC n) n) ⇔ ∀n. 0 < n ⇒ P n (n − 1)

SUC_ELIM_NUMERALS

⊢ ∀f g.
      (∀n. g (SUC n) = f n (SUC n)) ⇔
      (∀n. g (NUMERAL (BIT1 n)) = f (NUMERAL (BIT1 n) − 1) (NUMERAL (BIT1 n))) ∧
      ∀n. g (NUMERAL (BIT2 n)) = f (NUMERAL (BIT1 n)) (NUMERAL (BIT2 n))

SUB_ELIM_THM

⊢ P (a − b) ⇔ ∀d. (b = a + d ⇒ P 0) ∧ (a = b + d ⇒ P d)

PRE_ELIM_THM

⊢ P (PRE n) ⇔ ∀m. (n = 0 ⇒ P 0) ∧ (n = SUC m ⇒ P m)

MULT_INCREASES

⊢ ∀m n. 1 < m ∧ 0 < n ⇒ SUC n ≤ m * n

EXP_ALWAYS_BIG_ENOUGH

⊢ ∀b. 1 < b ⇒ ∀n. ∃m. n ≤ b ** m

EXP_EQ_0

⊢ ∀n m. n ** m = 0 ⇔ n = 0 ∧ 0 < m

ZERO_LT_EXP

⊢ 0 < x ** y ⇔ 0 < x ∨ y = 0

EXP_1

⊢ ∀n. 1 ** n = 1 ∧ n ** 1 = n

EXP_EQ_1

⊢ ∀n m. n ** m = 1 ⇔ n = 1 ∨ m = 0

EXP_BASE_LE_MONO

⊢ ∀b. 1 < b ⇒ ∀n m. b ** m ≤ b ** n ⇔ m ≤ n

EXP_BASE_LT_MONO

⊢ ∀b. 1 < b ⇒ ∀n m. b ** m < b ** n ⇔ m < n

EXP_BASE_INJECTIVE

⊢ ∀b. 1 < b ⇒ ∀n m. b ** n = b ** m ⇔ n = m

EXP_BASE_LEQ_MONO_IMP

⊢ ∀n m b. 0 < b ∧ m ≤ n ⇒ b ** m ≤ b ** n

EXP_BASE_LEQ_MONO_SUC_IMP

⊢ m ≤ n ⇒ SUC b ** m ≤ SUC b ** n

EXP_BASE_LE_IFF

⊢ b ** m ≤ b ** n ⇔ b = 0 ∧ n = 0 ∨ b = 0 ∧ 0 < m ∨ b = 1 ∨ 1 < b ∧ m ≤ n

X_LE_X_EXP

⊢ 0 < n ⇒ x ≤ x ** n

X_LT_EXP_X

⊢ 1 < b ⇒ x < b ** x

ZERO_EXP

⊢ 0 ** x = if x = 0 then 1 else 0

X_LT_EXP_X_IFF

⊢ x < b ** x ⇔ 1 < b ∨ x = 0

EXP_EXP_LT_MONO

⊢ ∀a b. a ** n < b ** n ⇔ a < b ∧ 0 < n

EXP_EXP_LE_MONO

⊢ ∀a b. a ** n ≤ b ** n ⇔ a ≤ b ∨ n = 0

EXP_EXP_INJECTIVE

⊢ ∀b1 b2 x. b1 ** x = b2 ** x ⇔ x = 0 ∨ b1 = b2

EXP_SUB

⊢ ∀p q n. 0 < n ∧ q ≤ p ⇒ n ** (p − q) = n ** p DIV n ** q

EXP_SUB_NUMERAL

⊢ 0 < n ⇒
  n ** NUMERAL (BIT1 x) DIV n = n ** (NUMERAL (BIT1 x) − 1) ∧
  n ** NUMERAL (BIT2 x) DIV n = n ** NUMERAL (BIT1 x)

EXP_BASE_MULT

⊢ ∀z x y. (x * y) ** z = x ** z * y ** z

EXP_EXP_MULT

⊢ ∀z x y. x ** (y * z) = (x ** y) ** z

MAX_COMM

⊢ ∀m n. MAX m n = MAX n m

MIN_COMM

⊢ ∀m n. MIN m n = MIN n m

MAX_ASSOC

⊢ ∀m n p. MAX m (MAX n p) = MAX (MAX m n) p

MIN_ASSOC

⊢ ∀m n p. MIN m (MIN n p) = MIN (MIN m n) p

MIN_MAX_EQ

⊢ ∀m n. MIN m n = MAX m n ⇔ m = n

MIN_MAX_LT

⊢ ∀m n. MIN m n < MAX m n ⇔ m ≠ n

MIN_MAX_LE

⊢ ∀m n. MIN m n ≤ MAX m n

MIN_MAX_PRED

⊢ ∀P m n. P m ∧ P n ⇒ P (MIN m n) ∧ P (MAX m n)

MIN_LT

⊢ ∀n m p. (MIN m n < p ⇔ m < p ∨ n < p) ∧ (p < MIN m n ⇔ p < m ∧ p < n)

MAX_LT

⊢ ∀n m p. (p < MAX m n ⇔ p < m ∨ p < n) ∧ (MAX m n < p ⇔ m < p ∧ n < p)

MIN_LE

⊢ ∀n m p. (MIN m n ≤ p ⇔ m ≤ p ∨ n ≤ p) ∧ (p ≤ MIN m n ⇔ p ≤ m ∧ p ≤ n)

MAX_LE

⊢ ∀n m p. (p ≤ MAX m n ⇔ p ≤ m ∨ p ≤ n) ∧ (MAX m n ≤ p ⇔ m ≤ p ∧ n ≤ p)

MIN_0

⊢ ∀n. MIN n 0 = 0 ∧ MIN 0 n = 0

MAX_0

⊢ ∀n. MAX n 0 = n ∧ MAX 0 n = n

MAX_EQ_0

⊢ MAX m n = 0 ⇔ m = 0 ∧ n = 0

MIN_EQ_0

⊢ MIN m n = 0 ⇔ m = 0 ∨ n = 0

MIN_IDEM

⊢ ∀n. MIN n n = n

MAX_IDEM

⊢ ∀n. MAX n n = n

EXISTS_GREATEST

⊢ ∀P. (∃x. P x) ∧ (∃x. ∀y. y > x ⇒ ¬P y) ⇔ ∃x. P x ∧ ∀y. y > x ⇒ ¬P y

EXISTS_NUM

⊢ ∀P. (∃n. P n) ⇔ P 0 ∨ ∃m. P (SUC m)

FORALL_NUM

⊢ ∀P. (∀n. P n) ⇔ P 0 ∧ ∀n. P (SUC n)

BOUNDED_FORALL_THM

⊢ ∀c. 0 < c ⇒ ((∀n. n < c ⇒ P n) ⇔ P (c − 1) ∧ ∀n. n < c − 1 ⇒ P n)

BOUNDED_EXISTS_THM

⊢ ∀c. 0 < c ⇒ ((∃n. n < c ∧ P n) ⇔ P (c − 1) ∨ ∃n. n < c − 1 ∧ P n)

transitive_monotone

⊢ ∀R f. transitive R ∧ (∀n. R (f n) (f (SUC n))) ⇒ ∀m n. m < n ⇒ R (f m) (f n)

STRICTLY_INCREASING_TC

⊢ ∀f. (∀n. f n < f (SUC n)) ⇒ ∀m n. m < n ⇒ f m < f n

STRICTLY_INCREASING_ONE_ONE

⊢ ∀f. (∀n. f n < f (SUC n)) ⇒ ONE_ONE f

ONE_ONE_INV_IMAGE_BOUNDED

⊢ ONE_ONE f ⇒ ∀b. ∃a. ∀x. f x ≤ b ⇒ x ≤ a

ONE_ONE_UNBOUNDED

⊢ ∀f. ONE_ONE f ⇒ ∀b. ∃n. b < f n

STRICTLY_INCREASING_UNBOUNDED

⊢ ∀f. (∀n. f n < f (SUC n)) ⇒ ∀b. ∃n. b < f n

NOT_STRICTLY_DECREASING

⊢ ∀f. ¬∀n. f (SUC n) < f n

ABS_DIFF_SYM

⊢ ∀n m. ABS_DIFF n m = ABS_DIFF m n

ABS_DIFF_COMM

⊢ ∀n m. ABS_DIFF n m = ABS_DIFF m n

ABS_DIFF_EQS

⊢ ∀n. ABS_DIFF n n = 0

ABS_DIFF_EQ_0

⊢ ∀n m. ABS_DIFF n m = 0 ⇔ n = m

ABS_DIFF_ZERO

⊢ ∀n. ABS_DIFF n 0 = n ∧ ABS_DIFF 0 n = n

ABS_DIFF_SUC

⊢ ∀n m. ABS_DIFF (SUC n) (SUC m) = ABS_DIFF n m

ABS_DIFF_SUC_LE

⊢ ∀x z. ABS_DIFF x (SUC z) ≤ SUC (ABS_DIFF x z)

ABS_DIFF_PLUS_LE

⊢ ∀x z y. ABS_DIFF x (y + z) ≤ y + ABS_DIFF x z

ABS_DIFF_LE_SUM

⊢ ABS_DIFF x z ≤ x + z

ABS_DIFF_TRIANGLE_lem

⊢ ∀x y. x ≤ ABS_DIFF x y + y

ABS_DIFF_TRIANGLE

⊢ ∀x y z. ABS_DIFF x z ≤ ABS_DIFF x y + ABS_DIFF y z

ABS_DIFF_ADD_SAME

⊢ ∀n m p. ABS_DIFF (n + p) (m + p) = ABS_DIFF n m

LE_SUB_RCANCEL

⊢ ∀m n p. n − m ≤ p − m ⇔ n ≤ m ∨ n ≤ p

LT_SUB_RCANCEL

⊢ ∀m n p. n − m < p − m ⇔ n < p ∧ m < p

LE_SUB_LCANCEL

⊢ ∀z y x. x − y ≤ x − z ⇔ z ≤ y ∨ x ≤ y

LT_SUB_LCANCEL

⊢ ∀z y x. x − y < x − z ⇔ z < y ∧ z < x

ABS_DIFF_SUMS

⊢ ∀n1 n2 m1 m2. ABS_DIFF (n1 + n2) (m1 + m2) ≤ ABS_DIFF n1 m1 + ABS_DIFF n2 m2

FUNPOW_SUC

⊢ ∀f n x. FUNPOW f (SUC n) x = f (FUNPOW f n x)

FUNPOW_0

⊢ FUNPOW f 0 x = x

FUNPOW_ADD

⊢ ∀m n. FUNPOW f (m + n) x = FUNPOW f m (FUNPOW f n x)

FUNPOW_1

⊢ FUNPOW f 1 x = f x

NRC_0

⊢ ∀R x y. NRC R 0 x y ⇔ x = y

NRC_1

⊢ NRC R 1 x y ⇔ R x y

NRC_ADD_I

⊢ ∀m n x y z. NRC R m x y ∧ NRC R n y z ⇒ NRC R (m + n) x z

NRC_ADD_E

⊢ ∀m n x z. NRC R (m + n) x z ⇒ ∃y. NRC R m x y ∧ NRC R n y z

NRC_ADD_EQN

⊢ NRC R (m + n) x z ⇔ ∃y. NRC R m x y ∧ NRC R n y z

NRC_SUC_RECURSE_LEFT

⊢ NRC R (SUC n) x y ⇔ ∃z. NRC R n x z ∧ R z y

NRC_RTC

⊢ ∀n x y. NRC R n x y ⇒ R^* x y

RTC_NRC

⊢ ∀x y. R^* x y ⇒ ∃n. NRC R n x y

RTC_eq_NRC

⊢ ∀R x y. R^* x y ⇔ ∃n. NRC R n x y

TC_eq_NRC

⊢ ∀R x y. R⁺ x y ⇔ ∃n. NRC R (SUC n) x y

LESS_EQUAL_DIFF

⊢ ∀m n. m ≤ n ⇒ ∃k. m = n − k

MOD_2

⊢ ∀n. n MOD 2 = if EVEN n then 0 else 1

EVEN_MOD2

⊢ ∀x. EVEN x ⇔ x MOD 2 = 0

SUC_MOD

⊢ ∀n a b. 0 < n ⇒ (SUC a MOD n = SUC b MOD n ⇔ a MOD n = b MOD n)

ADD_MOD

⊢ ∀n a b p. 0 < n ⇒ ((a + p) MOD n = (b + p) MOD n ⇔ a MOD n = b MOD n)

MOD_ELIM

⊢ ∀P x n. 0 < n ∧ P x ∧ (∀y. P (y + n) ⇒ P y) ⇒ P (x MOD n)

DOUBLE_LT

⊢ ∀p q. 2 * p + 1 < 2 * q ⇔ 2 * p < 2 * q

EXP2_LT

⊢ ∀m n. n DIV 2 < 2 ** m ⇔ n < 2 ** SUC m

SUB_LESS

⊢ ∀m n. 0 < n ∧ n ≤ m ⇒ m − n < m

SUB_MOD

⊢ ∀m n. 0 < n ∧ n ≤ m ⇒ (m − n) MOD n = m MOD n

ONE_LT_MULT_IMP

⊢ ∀p q. 1 < p ∧ 0 < q ⇒ 1 < p * q

ONE_LT_MULT

⊢ ∀x y. 1 < x * y ⇔ 0 < x ∧ 1 < y ∨ 0 < y ∧ 1 < x

ONE_LT_EXP

⊢ ∀x y. 1 < x ** y ⇔ 1 < x ∧ 0 < y

findq_thm

⊢ findq (a,m,n) = if n = 0 then a
  else (let d = 2 * n in if m < d then a else findq (2 * a,m,d))

findq_eq_0

⊢ ∀a m n. findq (a,m,n) = 0 ⇔ a = 0

findq_divisor

⊢ n ≤ m ⇒ findq (a,m,n) * n ≤ a * m

DIVMOD_THM

⊢ DIVMOD (a,m,n) = if n = 0 then (0,0) else if m < n then (a,m)
  else (let q = findq (1,m,n) in DIVMOD (a + q,m − n * q,n))

MOD_SUB

⊢ 0 < n ∧ n * q ≤ m ⇒ (m − n * q) MOD n = m MOD n

DIV_SUB

⊢ 0 < n ∧ n * q ≤ m ⇒ (m − n * q) DIV n = m DIV n − q

DIVMOD_CORRECT

⊢ ∀m n a. 0 < n ⇒ DIVMOD (a,m,n) = (a + m DIV n,m MOD n)

DIVMOD_CALC

⊢ (∀m n. 0 < n ⇒ m DIV n = FST (DIVMOD (0,m,n))) ∧
  ∀m n. 0 < n ⇒ m MOD n = SND (DIVMOD (0,m,n))

MODEQ_0_CONG

⊢ MODEQ 0 m1 m2 ⇔ m1 = m2

MODEQ_NONZERO_MODEQUALITY

⊢ 0 < n ⇒ (MODEQ n m1 m2 ⇔ m1 MOD n = m2 MOD n)

MODEQ_THM

⊢ MODEQ n m1 m2 ⇔ n = 0 ∧ m1 = m2 ∨ 0 < n ∧ m1 MOD n = m2 MOD n

MODEQ_INTRO_CONG

⊢ 0 < n ⇒ MODEQ n e0 e1 ⇒ e0 MOD n = e1 MOD n

MODEQ_PLUS_CONG

⊢ MODEQ n x0 x1 ⇒ MODEQ n y0 y1 ⇒ MODEQ n (x0 + y0) (x1 + y1)

MODEQ_MULT_CONG

⊢ MODEQ n x0 x1 ⇒ MODEQ n y0 y1 ⇒ MODEQ n (x0 * y0) (x1 * y1)

MODEQ_REFL

⊢ ∀x. MODEQ n x x

MODEQ_SUC_CONG

⊢ MODEQ n x y ⇒ MODEQ n (SUC x) (SUC y)

MODEQ_EXP_CONG

⊢ MODEQ n x y ⇒ MODEQ n (x ** e) (y ** e)

EXP_MOD

⊢ 0 < n ⇒ (x MOD n) ** e MOD n = x ** e MOD n

MODEQ_SYM

⊢ MODEQ n x y ⇔ MODEQ n y x

MODEQ_TRANS

⊢ ∀x y z. MODEQ n x y ∧ MODEQ n y z ⇒ MODEQ n x z

MODEQ_NUMERAL

⊢ (NUMERAL n ≤ NUMERAL m ⇒
   MODEQ (NUMERAL (BIT1 n)) (NUMERAL (BIT1 m))
     (NUMERAL (BIT1 m) MOD NUMERAL (BIT1 n))) ∧
  (NUMERAL n ≤ NUMERAL m ⇒
   MODEQ (NUMERAL (BIT1 n)) (NUMERAL (BIT2 m))
     (NUMERAL (BIT2 m) MOD NUMERAL (BIT1 n))) ∧
  (NUMERAL n ≤ NUMERAL m ⇒
   MODEQ (NUMERAL (BIT2 n)) (NUMERAL (BIT2 m))
     (NUMERAL (BIT2 m) MOD NUMERAL (BIT2 n))) ∧
  (NUMERAL n < NUMERAL m ⇒
   MODEQ (NUMERAL (BIT2 n)) (NUMERAL (BIT1 m))
     (NUMERAL (BIT1 m) MOD NUMERAL (BIT2 n)))

MODEQ_MOD

⊢ 0 < n ⇒ MODEQ n (x MOD n) x

MODEQ_0

⊢ 0 < n ⇒ MODEQ n n 0

num_case_eq

⊢ num_CASE n zc sc = v ⇔ n = 0 ∧ zc = v ∨ ∃x. n = SUC x ∧ sc x = v

datatype_num

⊢ DATATYPE (num 0 SUC)