Nuprl - Proof: mu-property

(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

f:(

). (

n:

. f(n))

f(mu(f)) & (

i:

. i<mu(f)

f(i))

By:	Assert (b:, f:(). (n:. nb & f(n)) f(mu(f)) & (i:. i<mu(f) f(i)))

Generated subgoals:

1   b:, f:(). (n:. nb & f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))
15 steps

2 1. b:, f:(). (n:. nb & f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))
  f:(). (n:. f(n))  f(mu(f)) & (i:. i<mu(f)  f(i))
3 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