At: strong switch inv decomposable 1 2 1 1 1 1
1. E: TaggedEventStruct
2. tr: |E| List
3. Causal(E)(tr)
4. AD-normal(E)(tr)
5. No-dup-deliver(E)(tr)
6. 
tr = nil
7. ls: 
||tr||
8. is-send(E)(tr[ls])
9. 
j:||tr||. ls < j 
is-send(E)(tr[j])
10. i:||tr||. (i (switchR(tr)^*) ls) is-send(E)(tr[i])
11. EquivRel(|E|)(_1 =msg=(E) _2)
12. i,j:||tr||. i
j is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls)
13. i: ||tr||
14. j: ||tr||
15. 0 = j-i
16. i (switchR(tr)^*) ls
17. ij
tr[i] =msg=(E) tr[j]
By:
Subst' (j = i) 0
THEN
UseEquiv
Generated subgoals:None
About:
