Nuprl - Proof: w-sender wf 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: w-sender wf 1

1. the_w : World
2. e : E
3. FairFifo
4. isrcv(kind(e))

. match(lnk(kind(e));n;time(e))

By:	AssertBY (n:time(e). match(lnk(kind(e));n;time(e))) (BackThru (Thm* the_w:World, e:E. (Thm* FairFifo (Thm* (Thm* isrcv(kind(e)) (t:time(e). match(lnk(kind(e));t;time(e)))) THEN ParallelOp -1

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html