IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
fincr wf1411111112 1. i :
2. f : {f | i:{z:| z<i } if i=0 else {f(i-1)...} fi}
3. j :
4. j1:. j1<jj1<if(j1)
5. j<i 6. y : if j=0 else {f(j-1)...} fi
7. y = f(j)
8. j 0
9. j:{f(j-1)...}. j f(j)
By:
With (f(j)) (Analyze -1)
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html