the_w:World. FairFifo 
Propthe_w:World, l:IdLnk, i:Id, a:Action(i).
Thm* isrcv(l;a)
isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = lthe_w:World, i:Id, a:Action(i), l:IdLnk. isrcv(l;a) msg(a) Msg| Rank | Theorem | Name |
| 2 | the_w:World. FairFifo Prop | [fair-fifo_wf] |
| cites the following: | ||
| 1 | the_w:World, l:IdLnk, i:Id, a:Action(i).
Thm* isrcv(l;a) isnull(a) & isrcv(kind(a)) & lnk(kind(a)) = l | [assert-w-isrcvl] |
| 0 | the_w:World, i:Id, a:Action(i), l:IdLnk. isrcv(l;a) msg(a) Msg | [w-msg_wf] |