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

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

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

Y(

f,x. g(x,f))

(

j:

r. P(j))

By:	Inclusion 6

Generated subgoals:

None

About:

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

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