the_w:World, e:E. FairFifo 
isrcv(kind(e)) sender(e) 
Ethe_w:World, e:E.
Thm* FairFifo
isrcv(kind(e)) (
t:
time(e). match(lnk(kind(e));t;time(e)))f:(
). (n:. f(n)) f(mu(f)) & (i:. i<mu(f) 
f(i))| Rank | Theorem | Name |
| 4 | the_w:World, e:E. FairFifo isrcv(kind(e)) sender(e) E | [w-sender_wf] |
| cites the following: | ||
| 3 | the_w:World, e:E.
Thm* FairFifo isrcv(kind(e)) (t:time(e). match(lnk(kind(e));t;time(e))) | [w-match-exists] |
| 0 | f:(). (n:. f(n)) f(mu(f)) & (i:. i<mu(f) f(i)) | [mu-property] |