Theory "num"

Signature

Definitions

IS_NUM_REP

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

SUC_DEF

⊢ ∀m. SUC m = ABS_num (SUC_REP (REP_num m))

SUC_REP_DEF

⊢ ONE_ONE SUC_REP ∧ ¬ONTO SUC_REP

ZERO_DEF

⊢ 0 = ABS_num ZERO_REP

ZERO_REP_DEF

⊢ ∀y. ZERO_REP ≠ SUC_REP y

num_ISO_DEF

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

num_TY_DEF

⊢ ∃rep. TYPE_DEFINITION IS_NUM_REP rep

Theorems

INDUCTION

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

INV_SUC

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

NOT_SUC

⊢ ∀n. SUC n ≠ 0