Nuprl - Proof: complete nat ind with y 1 1 2 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

1. P :

Prop
2. g :

i:

. (

j:

i. P(j))

P(i)
3. Y(

f,x. g(x,f))

Void

Void
4. n :

Y(

f,x. g(x,f))

(

m:

n. P(m))

By:	NInd 4 THEN IfLabL [`wf`,Auto ;RULE H C ext t BY arith Type{i} Let SubGoals; t = CallLisp(ARITH) SubGoals ;,Auto]

Generated subgoals:

1   Y(f,x. g(x,f))  (m:0. P(m))
4 steps

2 4. n :
5. 0<n
6. Y(f,x. g(x,f))  (m:(n-1). P(m))
  Y(f,x. g(x,f))  (m:n. P(m))
7 steps

About:

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

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