Theory prim_rec

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

⊢ ∀m. PRE m = if m = 0 then 0 else @n. m = SUC n

⊢ ∀x f m. PRIM_REC x f m = PRIM_REC_FUN x f m (PRE m)

⊢ ∀x f. PRIM_REC_FUN x f = SIMP_REC (λn. x) (λfun n. f (fun (PRE n)) n)

⊢ ∀x f' n. ∃g. SIMP_REC_REL g x f' (SUC n) ∧ SIMP_REC x f' n = g n

⊢ ∀fun x f n.
    SIMP_REC_REL fun x f n ⇔
    fun 0 = x ∧ ∀m. m < n ⇒ fun (SUC m) = f (fun m)

⊢ measure = inv_image $<

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

⊢ ∀R. Wellfounded R ⇔ ¬∃f. ∀n. R (f (SUC n)) (f n)

⊢ ∀P R a.
    P a ∧ (∀x. P x ⇒ ∃y. P y ∧ R x y) ⇒
    ∃f. f 0 = a ∧ ∀n. P (f n) ∧ R (f n) (f (SUC n))

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

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

⊢ ∀n. 0 < SUC n

⊢ 0 < SUC 0

⊢ $< = (λx y. y = SUC x)⁺

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

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

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

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

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

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

⊢ ∀n. ¬(n < n)

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

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

⊢ ∀n. n < SUC n

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

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

⊢ ∀n. ¬(n < 0)

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

⊢ PRE 0 = 0 ∧ ∀m. PRE (SUC m) = m

⊢ ∀x f.
    (∀n. PRIM_REC_FUN x f 0 n = x) ∧
    ∀m n. PRIM_REC_FUN x f (SUC m) n = f (PRIM_REC_FUN x f m (PRE n)) n

⊢ ∀x f.
    PRIM_REC x f 0 = x ∧ ∀m. PRIM_REC x f (SUC m) = f (PRIM_REC x f m) m

⊢ ∀m n. (λx y. y = f x)꙳ (f m) n ⇔ (λx y. y = f x)⁺ m n

⊢ ∀x f n. ∃fun. SIMP_REC_REL fun x f n

⊢ ∀x f g1 g2 m1 m2.
    SIMP_REC_REL g1 x f m1 ∧ SIMP_REC_REL g2 x f m2 ⇒
    ∀n. n < m1 ∧ n < m2 ⇒ g1 n = g2 n

⊢ ∀x f n. ∃!y. ∃g. SIMP_REC_REL g x f (SUC n) ∧ y = g n

⊢ ∀x f. SIMP_REC x f 0 = x ∧ ∀m. SIMP_REC x f (SUC m) = f (SIMP_REC x f m)

⊢ ∀n. SUC n ≠ n

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

⊢ ∀m n. (λx y. y = SUC x)⁺ m (SUC n) ⇔ (λx y. y = SUC x)꙳ m n

⊢ ∀R. WF R ⇔ Wellfounded R

⊢ WF $<

⊢ WF (λx y. y = SUC x)

⊢ ∀m. WF (measure m)

⊢ ∀f x y. measure f x y ⇔ f x < f y

⊢ ∀e f. ∃fn. fn 0 = e ∧ ∀n. fn (SUC n) = f n (fn n)

⊢ ∀e f. ∃!fn1. fn1 0 = e ∧ ∀n. fn1 (SUC n) = f (fn1 n) n