IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
least characterized211 1. k :
2. 0<k 3. p:{p:((k-1))| i:(k-1). p(i) }.
3. (least i:. p(i)) {i:(k-1)| p(i) & (j:i. p(j)) }
4. p : k 5. i : k 6. p(i)
7. p(0)
0 {i:k| p(i) & (j:i. p(j)) }
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html