Nuprl - Proof: mu wf 1

(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

b:

, f:(

). (

n:

. n

b & f(n))

mu(f)

By:	InductionOnNat THEN RepeatFor 2 (Analyze 0) THEN ExRepD THEN RecUnfold `mu` 0 THEN SplitOnConclITE

Generated subgoals:

1 1. f :
2. n :
3. n0
4. f(n)
5. f(0)
  mu(x.f(x+1))+1
1 step

2 1. b :
2. 0<b
3. f:(). (n:. nb-1 & f(n))  mu(f)
4. f :
5. n :
6. nb
7. f(n)
8. f(0)
  mu(x.f(x+1))+1
6 steps

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