Nuprl - Proof: comp nat ind tp 1 1 1 1 1 1 2 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. P :

Prop
2.

. (

. j<i

P(j))

P(i)
3. zz :

4. 0<zz
5.

. i<zz-1

P(i)
6. i :

7. i<zz

i1:

. i1<i

P(i1)

By:	(Analyze 0) THEN (Analyze 0)

Generated subgoals:

1 8. i1 :
9. i1<i
  P(i1)
3 steps

2 1. P : Prop{k}
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 :
  (i1<i)  Prop{1}
1 step

3 1. P : Prop{k}
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
    Type{1}
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

1	8. i1 : 9. i1<i P(i1)	3 steps
2	1. P : Prop{k} 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 : (i1<i) Prop{1}	1 step
3	1. P : Prop{k} 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 Type{1}	1 step