2. FairFifo
3.
e,e':E. loc(e) = loc(e') 
e <c e' 
e = e' e' <c e
4.
e:E. first(e) 
(e':E. loc(e') = loc(e) 
e' <c e)
5.
e:E.
5.
first(e)
5.
5. loc(pred(e)) = loc(e) & pred(e) <c e
5. & (
e':E. loc(e') = loc(e) (pred(e) <c e' & e' <c e))
6. t :
7. 0<t
8.
i:Id. first(<i,t-1>) (x:Id. (x when <i,t-1>) = (x after pred(<i,t-1>)))
9.
t = 0
10. i : Id
11. isnull(a(i;t-1))
12. first(<i,t-1>)
13.
first(<i,t-1>)
14.
x:Id. (x when <i,t-1>) = (x after pred(<i,t-1>))
15. x@0 : Id
16. (x@0 when <i,t-1>) = (x@0 after pred(<i,t-1>))
s(i;t).x@0 = s(i;t-1).x@0 vartype(i;x@0)
