1 | 1. E: TaggedEventStruct 2. tr: |E| List 3. switch_inv(E)(tr) 4. Causal(E)(tr) 5. AD-normal(E)(tr) 6. No-dup-deliver(E)(tr) 7. tr = nil Q:( ||tr|| Prop).
( i: ||tr||. Dec(Q(i)))
& ( i: ||tr||. Q(i))
& ( i: ||tr||. Q(i)  is-send(E)(tr[i]))
& ( i,j: ||tr||. Q(i)  Q(j)  tag(E)(tr[i]) = tag(E)(tr[j]))
& ( i,j: ||tr||. Q(i)  i j  C(Q)(j)) |