Nuprl - Proof: fair-fifo wf 1 1 1

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

1. the_w : World
2. i : Id
3. t :

4. l : IdLnk
5. isrcv(l;a(i;t))
6. ||queue(l;t)||

1
7.

isnull(a(i;t))
8. isrcv(kind(a(i;t)))
9. lnk(kind(a(i;t))) = l

isrcv(lnk(kind(a(i;t)));a(i;t))

By:	HypSubst -1 0

Generated subgoals:

None

About:

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