Nuprl Basics - Proof: kleene minimize is lb 1

(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

n:

, f:{f:(

)|

x:

. f(x) }. mu(f) = n

(

i:

. i<mu(f)

f(i))

By:	CompNatInd Concl

Generated subgoal:

1 1. n :
2. n1:.
2. n1<n (f:{f:()| x:. f(x) }. mu(f) = n1 (i:. i<mu(f) f(i)))
f:{f:()| x:. f(x) }. mu(f) = n (i:. i<mu(f) f(i))
7 steps

About:

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

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