IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
least characterized
2
1
2
2
1
1
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)
8. (least i:
. p(i+1))
(k-1)
9. p((least i:
. p(i+1))+1)
10.
j:
(least i:
. p(i+1)).
p(j+1)
11. (least i:
. p(i+1))
12. j :
((least i:
. p(i+1))+1)
p(j)
By: |
Decide: j = 0 k |
Generated subgoals:
1 |
13. j = 0 k
p(j)
 | 1 step |
2 |
13. j = 0 k
p(j)
 | 1 step |
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html