2.
n1:. n1<n 
(f:{f:(
)| 
x:. f(x) }. mu(f) = n1 f(mu(f)))
3. f : {f:(
)| x:. f(x) }
4. mu(f) = n
f(mu(f))
n1:. n1<n (f:{f:()| x:. f(x) }. mu(f) = n1 f(mu(f)))
)| x:. f(x) }
f(mu(f))| By: |
if f(0) 0 else 1+mu( x.f(1+x)) fi THEN SplitOnConclITE |
| 1 |
 f(0)
f(1+mu(x.f(1+x))) | 3 steps |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |