| Parents |
| wf_rel |
| Constants |
|
is_recfun
|
(('a  'a) SET  'a ('a ('a 'a) SET  'a) ('a 'a) SET) SET
|
|
the_recfun
|
('a 'a) SET 'a ('a ('a 'a) SET 'a) ('a 'a) SET
|
|
wftrecfun
|
('a 'a) SET ('a ('a 'a) SET 'a) ('a 'a) SET
|
|
wftrec
|
('a 'a) SET 'a ('a ('a 'a) SET '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)
|
