Theory "arithmetic"

Parents pair prim_rec

Signature

Constant	Type
num_case	:'a -> (num -> 'a) -> num -> 'a
nat_elim__magic	:num -> num
findq	:num # num # num -> num
ZERO	:num
ODD	:num -> bool
NUMERAL	:num -> num
MOD_2EXP	:num -> num -> num
MOD	:num -> num -> num
MIN	:num -> num -> num
MAX	:num -> num -> num
FUNPOW	:('a -> 'a) -> num -> 'a -> 'a
FACT	:num -> num
EXP	:num -> num -> num
EVEN	:num -> bool
DIV_2EXP	:num -> num -> num
DIVMOD	:num # num # num -> num # num
DIV2	:num -> num
DIV	:num -> num -> num
BIT2	:num -> num
BIT1	:num -> num
>=	:num -> num -> bool
>	:num -> num -> bool
<=	:num -> num -> bool
-	:num -> num -> num
+	:num -> num -> num
*	:num -> 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. _ inject_number 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

|- (!b f. num_case b f 0 = b) /\ !b f n. num_case b f (SUC n) = f n

FUNPOW

|- (!f x. FUNPOW f 0 x = x) /\ !f n x. FUNPOW f (SUC n) x = FUNPOW f n (f x)

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

MOD_2EXP_def

|- !x n. MOD_2EXP x n = n MOD 2 ** x

DIV_2EXP_def

|- !x n. DIV_2EXP x n = n DIV 2 ** x

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)

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

Theorems

ONE

|- 1 = SUC 0

TWO

|- 2 = SUC 1

NORM_0

|- 0 = 0

num_case_compute

|- !n. num_case f g n = (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

LESS_ADD

|- !m n. n < m ==> ?p. p + n = m

LESS_TRANS

|- !m n p. m < n /\ n < p ==> m < p

LESS_ANTISYM

|- !m n. ~(m < n /\ n < m)

LESS_LESS_SUC

|- !m n. ~(m < n /\ n < SUC m)

FUN_EQ_LEMMA

|- !f x1 x2. f x1 /\ ~f x2 ==> ~(x1 = x2)

LESS_MONO_REV

|- !m n. SUC m < SUC n ==> m < n

LESS_MONO_EQ

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

LESS_OR

|- !m n. m < n ==> SUC m <= n

OR_LESS

|- !m n. SUC m <= n ==> m < n

LESS_EQ

|- !m n. m < n = SUC m <= 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_SUC_REFL

|- !m. m <= SUC m

LESS_ADD_NONZERO

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

LESS_EQ_ANTISYM

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

NOT_LESS

|- !m n. ~(m < n) = n <= m

SUB_0

|- !m. (0 - m = 0) /\ (m - 0 = 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_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)

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)

LESS_EQUAL_ANTISYM

|- !n m. n <= m /\ m <= n ==> (n = m)

LESS_ADD_SUC

|- !m n. m < m + SUC n

ZERO_LESS_EQ

|- !n. 0 <= n

LESS_EQ_MONO

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

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)

SUB_MONO_EQ

|- !n m. SUC n - SUC m = n - m

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

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)

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)

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

LESS_EQ_IMP_LESS_SUC

|- !n m. n <= m ==> n < SUC m

SUB_LESS_EQ_ADD

|- !m p. m <= p ==> !n. p - m <= n = p <= m + n

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

NOT_LESS_EQUAL

|- !m n. ~(m <= n) = n < m

LESS_EQ_0

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

MULT_EQ_0

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

MULT_EQ_1

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

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

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

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

|- !m n. 0 < n /\ EVEN m ==> EVEN (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_SUC_LESS_EQ_0

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

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

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

DIV_LESS

|- !n d. 0 < n /\ 1 < d ==> n DIV d < 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_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))

num_case_cong

|- !M M' b f.
     (M = M') /\ ((M' = 0) ==> (b = b')) /\
     (!n. (M' = SUC n) ==> (f n = f' n)) ==>
     (num_case b f M = num_case b' f' M')

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

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)

FUNPOW_SUC

|- !f n x. FUNPOW f (SUC n) x = f (FUNPOW f n x)

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

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)

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