(10steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: kleene minimize is lb 1 1 1 1 1 2

1. n : 
2. n1:
2. n1<n  (f:{f:()| x:f(x) }. mu(f) = n1  (i:i<mu(f f(i)))
3. f : {f:()| x:f(x) }
4. f(0)
5. 1+mu(x.f(1+x)) = n
6. i : 
7. i<1+mu(x.f(1+x))
8. (x.f(1+x))  {f:()| x:f(x) }
9. i = 0
  f(i)


By: Inst: Hyp:2 Using:[mu(x.f(1+x)) | x.f(1+x) | i-1]


Generated subgoal:

1 10. (x.f(1+x))(i-1)
  f(i)

1 step

About:
boolassertintnatural_numberaddsubtractless_thansetlambdaapply
functionequalmemberimpliesallexists
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(10steps total) PrintForm Definitions Lemmas NuprlPrimitives Sections NuprlLIB Doc