At: switch normal exists 1 1
1. E: TaggedEventStruct
2. tr: |E| List
3. switch_inv(E)(tr)
4. No-dup-send(E)(tr)
5. EquivRel(|E|)(_1 =msg=(E) _2)
6. x: |E|
7. y: |E|
8. 
is-send(E)(y)
9. is-send(E)(x)
10. x1: 
||tr||
11. y1: ||tr||
12. x1 < y1
13. is-send(E)(tr[x1])
14. is-send(E)(tr[y1])
15. tr[x1] =msg=(E) x
16. tr[y1] =msg=(E) y
17. loc(E)(y) = loc(E)(x)
18. x@0: ||tr||
19. y@0: ||tr||
20. x@0 < y@0
21. is-send(E)(tr[x@0])
22. is-send(E)(tr[y@0])
23. tr[x@0] =msg=(E) y
24. tr[y@0] =msg=(E) x
loc(E)(x) = loc(E)(y)
By: AllHyps
(
h.
((((Unfold `no_duplicate_send` h) THEN (Reduce h) THEN (InstHyp [y1;x@0] h))
THENA
(Auto THEN (UseTrans y) THEN UseSym))
THEN
(InstHyp [x1;y@0] h))
THENA
(Auto THEN (UseTrans x) THEN UseSym))
Generated subgoals:None
About:
