(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

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) }
  f(i)


By: Decide: i = 0


Generated subgoals:

1 9. i = 0
  f(i)

1 step
2 9. i = 0
  f(i)

2 steps

About:
boolassertintnatural_numberaddless_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