Nuprl - Proof: complete nat ind with y 1 1 2 1 1 2 1 1 1

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

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: complete nat ind with y 1 1 2 1 1 2 1 1 1

1. P :

Prop
2. g :

i:

. (

j:

i. P(j))

P(i)
3. Y(

f,x. g(x,f))

Void

Void
4. n :

5. 0<n
6. Y(

f,x. g(x,f))

(

m:

(n-1). P(m))
7. r :

n
8. r = n-1

g(r,Y(

f,x. g(x,f)))

P(r)

By:	MemberEqCD

Generated subgoals:

1 g(r) (j:r. P(j))P(r)
Auto

2 Y(f,x. g(x,f)) (j:r. P(j))
1 step

About:

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

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