2.
n1:.
2. n1<n
(f:{f:(
)| 
x:. f(x) }. mu(f) = n1 (i:. i<mu(f) 
f(i)))
3. f : {f:(
)| x:. f(x) }
if f(0)
0 else 1+mu(
x.f(1+x)) fi = n 
(i:. i<if f(0) 0 else 1+mu(x.f(1+x)) fi f(i))
n1:.
(f:{f:()| x:. f(x) }. mu(f) = n1 (i:. i<mu(f) f(i)))
)| x:. f(x) }
if f(0) 0 else 1+mu(x.f(1+x)) fi = n
(i:. i<if f(0) 0 else 1+mu(x.f(1+x)) fi f(i))| By: |
THEN Try FwdThru: Thm* f:{f:()| x:. f(x) }. f(0) (x.f(1+x)) {f:()| x:. f(x) }
on [ f(0) ] |
| 1 |
f(0)
5. 1+mu( x.f(1+x)) = n
6. i :
7. i<1+mu( x.f(1+x))
8. ( x.f(1+x)) {f:()| x:. f(x) }
f(i) | 4 steps |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |