Theory num

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

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

⊢ ONE_ONE SUC_REP ∧ ¬ONTO SUC_REP

⊢ 0 = ABS_num ZERO_REP

⊢ ∀y. ZERO_REP ≠ SUC_REP y

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

⊢ ∃rep. TYPE_DEFINITION IS_NUM_REP rep

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

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

⊢ ∀n. SUC n ≠ 0