Nuprl - Proof: mu wf

(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

f:(

). (

n:

. f(n))

mu(f)

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

Generated subgoals:

1   b:, f:(). (n:. nb & f(n))  mu(f)
8 steps

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