the_w:World, e:E, t,t':
.
Thm* FairFifo
Thm*
Thm* isrcv(kind(e))
Thm*
Thm* match(lnk(kind(e));t;time(e))
match(lnk(kind(e));t';time(e)) t = t'the_w:World, l:IdLnk, t,t':.
Thm* match(l;t;t')
Thm*
Thm* ||snds(l;t)||
||rcvs(l;t')||
Thm* & ||rcvs(l;t')||<||snds(l;t)||+||onlnk(l;m(source(l);t))||
as,bs:T List. ||as @ bs|| = ||as||+||bs|| 
l1,l2:T List. l1 l2 ||l1||||l2||f:(
(T List)), t,t':.
Thm* t<t'
concat(map(f;upto(t))) @ (f(t)) concat(map(f;upto(t')))