Theory "num"

Signature

Definitions

SUC_REP_DEF

|- ONE_ONE SUC_REP ∧ ¬ONTO SUC_REP

ZERO_REP_DEF

|- ∀y. ZERO_REP ≠ SUC_REP y

IS_NUM_REP

|- ∀m. IS_NUM_REP m ⇔ ∀P. P ZERO_REP ∧ (∀n. P n ⇒ P (SUC_REP n)) ⇒ P m

num_TY_DEF

|- ∃rep. TYPE_DEFINITION IS_NUM_REP rep

num_ISO_DEF

|- (∀a. ABS_num (REP_num a) = a) ∧
   ∀r. IS_NUM_REP r ⇔ (REP_num (ABS_num r) = r)

ZERO_DEF

|- 0 = ABS_num ZERO_REP

SUC_DEF

|- ∀m. SUC m = ABS_num (SUC_REP (REP_num m))

Theorems

NOT_SUC

|- ∀n. SUC n ≠ 0

INV_SUC

|- ∀m n. (SUC m = SUC n) ⇒ (m = n)

INDUCTION

|- ∀P. P 0 ∧ (∀n. P n ⇒ P (SUC n)) ⇒ ∀n. P n