Thm* E:EventStruct, a,b:|E|, tr:|E| List.
a somewhere delivered before b

( k: ||tr||.
a delivered at time k 
( k': ||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k]))) | [not_delivered_before_somewhere] |
Def switch_inv(E)(tr)
== i,j,k: ||tr||.
i < j 
(is-send(E)(tr[i])) 
(is-send(E)(tr[j])) 
tag(E)(tr[i]) = tag(E)(tr[j]) 
tr[j] delivered at time k 
( k': ||tr||. k' < k & tr[i] delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k])) | [switch_inv] |
Def AD-normal(E)(tr)
== i: (||tr||-1).
( (is-send(E)(tr[i]))   (is-send(E)(tr[(i+1)]))  (tr[i] =msg=(E) tr[(i+1)]))
& (( x,y: ||tr||.
x < y
& (is-send(E)(tr[x]))
& (is-send(E)(tr[y]))
& tr[x] delivered at time i+1
& tr[y] delivered at time i)

loc(E)(tr[i]) = loc(E)(tr[(i+1)])) | [switch_normal] |
Def x somewhere delivered before y
== k: ||tr||.
x delivered at time k
& ( k': ||tr||. y delivered at time k'  loc(E)(tr[k']) = loc(E)(tr[k])  k k') | [delivered_before_somewhere] |