IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
mu-property1422112 1. b : 2. 0<b 3. f:(). (n:. nb-1 & f(n)) f(mu(f)) & (i:. i<mu(f) f(i))
4. f : 5. n : 6. nb 7. f(n)
8. f(0)
9. n = 0
10. f(mu(x.f(x+1))+1)
11. i:. i<mu(x.f(x+1)) f(i+1)
12. i : 13. i<mu(x.f(x+1))+1
14. i = 0
15. f(i-1+1)
f(i)
By:
ArithSimp -1
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html