At: P causal switchable0 2 1 2 2 1 1 1 2 1 1
1. E: EventStruct
2. x: |E| List
3. y: |E| List
4. 
tr':|E| List. tr' 
x 
(x
tr'.(
ytr'.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
9. tr: |E| List
10. tr x
11. tr' = filter(b.(b =msg=(E) a);tr)
12. x:|E|. (x tr) (ytr.is-send(E)(y) & (y =msg=(E) x))
13. x1: |E|
14. (x1 tr')
15. y1: |E|
16. (y1 tr)
17. is-send(E)(y1)
18. y1 =msg=(E) x1
19. y1 =msg=(E) a
20. (x1 tr)
x1 =msg=(E) a
By:
Inst
Thm* E:EventStruct. EquivRel(|E|)(_1 =msg=(E) _2)
[E]
THEN
UseTrans y1
THEN
UseSym
Generated subgoals:None
About:
