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
fill• (r, a, H, f) ∈ is_recfun
fill⇔ f
fill= {(x, y)
fill|(x, a) ∈ r
fill∧ y
fill= H
fill(x, {(v, w)|(v, w) ∈ f ∧ (v, x) ∈ r})}
the_recfun
⊢ ∀ r a H
fill• r ∈ twf
fill⇒ (r, a, H, the_recfun (r, a, H)) ∈ is_recfun
wftrecfun
⊢ ∀ r H
fill• wftrecfun (r, H)
fill= {(a, v)|v = H (a, the_recfun (r, a, H))}
wftrec
⊢ ∀ r a H
fill• wftrec (r, a, H) = H (a, the_recfun (r, a, H))
Theorems
ri_lemma
⊢ ∀ r H a f b g
fill• r ∈ twf
fill∧ (r, a, H, f) ∈ is_recfun
fill∧ (r, b, H, g) ∈ is_recfun
fill⇒ (∀ x
fill• (x, a) ∈ r ∧ (x, b) ∈ r
fill⇒ (∀ y• (x, y) ∈ f ⇔ (x, y) ∈ g))
recfun_Dom_thm
⊢ ∀ r a H f
fill• (r, a, H, f) ∈ is_recfun ⇒ Dom f = {x|(x, a) ∈ r}
recfun_unique_thm
⊢ ∀ r H a f g
fill• r ∈ twf
fill∧ (r, a, H, f) ∈ is_recfun
fill∧ (r, a, H, g) ∈ is_recfun
fill⇒ f = g
recfun_restr_lemma
⊢ ∀ r H a f b g
fill• r ∈ twf
fill∧ (r, a, H, f) ∈ is_recfun
fill∧ (r, b, H, g) ∈ is_recfun
fill∧ (a, b) ∈ r
fill⇒ f = Dom f ⊲ g
restr_is_recfun_lemma
⊢ ∀ r H a f b
fill• r ∈ twf ∧ (r, a, H, f) ∈ is_recfun ∧ (b, a) ∈ r
fill⇒ (r, b, H, {(v, w)|(v, w) ∈ f ∧ (v, b) ∈ r})
fill∈ is_recfun
exists_recfun_thm
⊢ ∀ H R a• R ∈ twf ⇒ (∃ f• (R, a, H, f) ∈ is_recfun)

up quick index

privacy policy

Created:

V