Nuprl - Proof: mu-property 1

(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

b:

, f:(

). (

n:

. n

b & f(n))

f(mu(f)) & (

i:

. i<mu(f)

f(i))

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)
  f(0) & (i:. i<0  f(i))
Auto

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

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

4 1. b :
2. 0<b
3. f:(). (n:. nb-1 & f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))
4. f :
5. n :
6. nb
7. f(n)
8. f(0)
  f(mu(x.f(x+1))+1) & (i:. i<mu(x.f(x+1))+1  f(i))
11 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