At: P causal switchable0 2 1 1 1
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4.
tr':|E| List. tr'
x 
(
x
tr'.(
y
tr'.is-send(E)(y) & (y =msg=(E) x)))
5. a: |E|
6. y = filter(
b.
(b =msg=(E) a);x)
7. tr': |E| List
8. tr'
y
tr'
filter(
b.
(b =msg=(E) a);x)
By: RevHypSubst -3 0
Generated subgoals:None
About: