Nuprl Basics - Proof: kleene minimize is lb

(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

f:{f:(

)|

x:

. f(x) }, i:

. i<mu(f)

f(i)

By:	n:, f:{f:()\| x:. f(x) }. mu(f) = n (i:. i<mu(f) f(i)) Asserted

Generated subgoals:

1   n:, f:{f:()| x:. f(x) }. mu(f) = n  (i:. i<mu(f)  f(i))
8 steps

2 1. n:, f:{f:()| x:. f(x) }. mu(f) = n  (i:. i<mu(f)  f(i))
  f:{f:()| x:. f(x) }, i:. i<mu(f)  f(i)
1 step

About:

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

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