Nuprl - Proof: mu-property 1 4

(19steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: mu-property 1 4

1. b :

2. 0<b
3.

f:(

). (

n:

. n

b-1 & f(n))

f(mu(f)) & (

i:

. i<mu(f)

f(i))
4. f :

5. n :

6. n

b
7. f(n)
8.

f(0)

f(mu(

x.f(x+1))+1) & (

i:

. i<mu(

x.f(x+1))+1

f(i))

By:	CaseNat 0 `n'

Generated subgoals:

1 9. n = 0
f(mu(x.f(x+1))+1) & (i:. i<mu(x.f(x+1))+1 f(i))
1 step

2 9. n = 0
f(mu(x.f(x+1))+1) & (i:. i<mu(x.f(x+1))+1 f(i))
9 steps

About:

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

(19steps total) PrintForm Definitions mb event system 1 Sections EventSystems Doc