2. L: |E| List
3.
L = nil4. Causal(E)(L)
5. x: |E|
6. (x
L)
i:
||L||. is-send(E)(L[i]) 
E:EventStruct, L:|E| List. L = nil 
Causal(E)(L) (i:||L||. is-send(E)(L[i]))L:T List. L = nil (x:T. (x L))
[-2]
| 1 | 1. E: EventStruct 2. L: |E| List 3. L = nil4. Causal(E)(L) 5. x: |E| 6. (x L) i:||L||. is-send(E)(L[i]) |
About:
 |  |  |  |  |  |  |  |  |