The Theory wf_rec
 Parents
 wf_rel
 Constants
 is_recfun ('a ↔ 'a) ↔ ('a × ('a × 'a ↔ 'a → 'a) × 'a ↔ 'a) the_recfun 'a ↔ 'a × 'a × ('a × 'a ↔ 'a → 'a) → 'a ↔ 'a wftrecfun 'a ↔ 'a × ('a × 'a ↔ 'a → 'a) → 'a ↔ 'a wftrec 'a ↔ 'a × 'a × ('a × 'a ↔ 'a → 'a) → 'a
 Definitions
 is_recfun ⊢ ∀ r a H f • (r, a, H, f) ∈ is_recfun ⇔ f = {(x, y) |(x, a) ∈ r ∧ y = H (x, {(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r})} the_recfun ⊢ ∀ r a H • r ∈ twf ⇒ (r, a, H, the_recfun (r, a, H)) ∈ is_recfun wftrecfun ⊢ ∀ r H • wftrecfun (r, H) = {(a, v)|v = H (a, the_recfun (r, a, H))} wftrec ⊢ ∀ r a H • wftrec (r, a, H) = H (a, the_recfun (r, a, H))
 Theorems
 ri_lemma ⊢ ∀ r H a f b g • r ∈ twf ∧ (r, a, H, f) ∈ is_recfun ∧ (r, b, H, g) ∈ is_recfun ⇒ (∀ x • (x, a) ∈ r ∧ (x, b) ∈ r ⇒ (∀ y• (x, y) ∈ f ⇔ (x, y) ∈ g)) recfun_Dom_thm ⊢ ∀ r a H f • (r, a, H, f) ∈ is_recfun ⇒ Dom f = {x|(x, a) ∈ r} recfun_unique_thm ⊢ ∀ r H a f g • r ∈ twf ∧ (r, a, H, f) ∈ is_recfun ∧ (r, a, H, g) ∈ is_recfun ⇒ f = g recfun_restr_lemma ⊢ ∀ r H a f b g • r ∈ twf ∧ (r, a, H, f) ∈ is_recfun ∧ (r, b, H, g) ∈ is_recfun ∧ (a, b) ∈ r ⇒ f = Dom f ⊲ g restr_is_recfun_lemma ⊢ ∀ r H a f b • r ∈ twf ∧ (r, a, H, f) ∈ is_recfun ∧ (b, a) ∈ r ⇒ (r, b, H, {(v, w)|(v, w) ∈ f ∧ (v, b) ∈ r}) ∈ is_recfun exists_recfun_thm ⊢ ∀ H R a• R ∈ twf ⇒ (∃ f• (R, a, H, f) ∈ is_recfun)