Nuprl - Proof: comp nat ind tp 1 1 1 1 1 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: comp nat ind tp 1 1 1 1 1 1

1. P :

Prop
2.

. (

. j<i

P(j))

P(i)
3. zz :

. i<zz

P(i)

By:

NatInd -1

Generated subgoals:

1   i:. i<0  P(i)
4 steps

2 3. zz :
4. 0<zz
5. i:. i<zz-1  P(i)
  i:. i<zz  P(i)
12 steps

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	i:. i<0 P(i)	4 steps
2	3. zz : 4. 0<zz 5. i:. i<zz-1 P(i) i:. i<zz P(i)	12 steps