At: switch decomp implies single tag decomp 3 1 1
1. E: TaggedEventStruct
2. tr: |E| List
3. Q: 
||tr||
Prop
4. 
i:||tr||. Dec(Q(i))
5. i: ||tr||
6. Q(i)
7. i:||tr||. Q(i) 
is-send(E)(tr[i])
8. i,j:||tr||. Q(i) Q(j) tag(E)(tr[i]) = tag(E)(tr[j])
9. i,j:||tr||. Q(i) i
j C(Q)(j)
10. i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j])
11. Causal(E)(tr)
12. No-dup-send(E)(tr)
13. 
tr = nil
14. L_1: |E| List
15. L_2: |E| List
16. tr = (L_1 @ L_2)
17. i:||tr||. (
k:||tr||. Q(k) & (tr[k] =msg=(E) tr[i])) 
||L_1||i
||tr|| = ||L_1||+||L_2||
By:
SubstFor tr 0
THEN
BackThru
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs||
Generated subgoals:None
About:
