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