Nuprl - Proof: mu-property 2

(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 2

1.

b:

, f:(

). (

n:

. n

b & f(n))

f(mu(f)) & (

i:

. i<mu(f)

f(i))

f:(

). (

n:

. f(n))

f(mu(f)) & (

i:

. i<mu(f)

f(i))

By:	Auto THEN ExRepD THEN InstHyp [n;f] 1

Generated subgoals:

1 2. f :
3. n :
4. f(n)
  n@0:. n@0n & f(n@0)
1 step

2 2. f :
3. n :
4. f(n)
5. f(mu(f)) & (i:. i<mu(f)  f(i))
  f(mu(f)) & (i:. i<mu(f)  f(i))
Trivial

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