2. FairFifo
3.
e,z:E. e <loc z 
isrcv(kind(z)) & e = sender(z) 
time(e)<time(z)
4. n :
5. 0<n
6. 0<n-1
6.
6. (
e,e':E.
6. ((e
e,e'. e <loc e' isrcv(kind(e')) & e = sender(e')^n-1 e')
6. (
6. (time(e)<time(e'))
7.
n = 1
8. 0<n
9.
n=
0
e,e':E.
(e
((x,y. 
z:E.
((x <loc z isrcv(kind(z)) & x = sender(z) 
E
((& (z e,e'. e <loc e' isrcv(kind(e')) & e = sender(e') E^n-1 y)) e')
time(e)<time(e')
