Nuprl - Proof: mu wf 1 2 2

(12steps 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 wf 1 2 2

1. b :

2. 0<b
3.

f:(

). (

n:

. n

b-1 & f(n))

mu(f)

4. f :

5. n :

6. n

b
7. f(n)
8.

f(0)
9.

n = 0

mu(

x.f(x+1))+1

By:	Assert (mu(x.f(x+1)) )

Generated subgoals:

1   mu(x.f(x+1))
2 steps

2 10. mu(x.f(x+1))
  mu(x.f(x+1))+1
1 step

About:

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

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