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

(35steps total) PrintForm Definitions int 1 Sections StandardLIB Doc

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 2 1 1 1

1. P :

Prop
2.

i:

. (

j:

. j<i

P(j))

P(i)
3. zz :

4. 0<zz
5.

i:

. i<zz-1

P(i)
6. i :

7. i<zz
8. i1 :

9. i1<i

P(i1)

By:	p.let i1 var_of_hyp -2 p in DTerm (mvt i1) -5 p

Generated subgoals:

1 5. i :
6. i<zz
7. i1 :
8. i1<i
  i1
1 step

2 5. i :
6. i<zz
7. i1 :
8. i1<i
9. i1<zz-1  P(i1)
  P(i1)
1 step

About:

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

(35steps total) PrintForm Definitions int 1 Sections StandardLIB Doc