| 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) |
