Nuprl - Proof: comp nat ind a 1 1

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

1. P :

Prop
2.

. (

. j<i

P(j))

P(i)
3.

j,s:

. s<j

P(s)

By:	(BackThru Thm* P:(Prop). P(0) (i:. P(i-1) P(i)) (i:. P(i))) THEN RepD

Generated subgoals:

1 4. s :
5. s<0
  P(s)
Auto

2 4. j :
5. s:. s<j-1  P(s)
6. s :
7. s<j
  P(s)
2 steps

About:

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

1	4. s : 5. s<0 P(s)	Auto
2	4. j : 5. s:. s<j-1 P(s) 6. s : 7. s<j P(s)	2 steps