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