f:{f:(
)| 
x:. f(x) }. f(mu(f))f:{f:()| x:. f(x) }. 
f(0) 
(
x.f(1+x)) 
{f:()| x:. f(x) }b:, x,y:T. b if b
x else y fi = y| Theorem | Name |
| f:{f:()| x:. f(x) }. f(mu(f)) | [kleene_minimize_is_fp] |
| cites the following: | |
| f:{f:()| x:. f(x) }. f(0) (x.f(1+x)) {f:()| x:. f(x) } | [kleene_tail] |
| b:, x,y:T. b if b x else y fi = y | [ite_rw_false] |