At: P causal switchable0 4 2 2
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. 
i:
||x||. 
j:||x||. j
i & is-send(E)(x[j]) & (x[j] =msg=(E) x[i])
5. x@0: |E|
6. is-send(E)(x@0)
7. y = (x @ [x@0])
8. i: ||y||
9. ||y|| = ||x||+1
10. 
i < ||x||
y[i] =msg=(E) y[i]
By:
Inst
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)
[E]
THEN
UseEquiv
Generated subgoals:None
About:
