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])))

1	1. E: EventStruct 2. a: |E| 3. b: |E| 4. tr: |E| List 5. a somewhere delivered before b 6. k: ||tr|| 7. a delivered at time k k':||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k])
2	1. E: EventStruct 2. a: |E| 3. b: |E| 4. tr: |E| List 5. k:||tr||. a delivered at time k (k':||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k])) a somewhere delivered before b

About: