(33steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: switch decomp implies single tag decomp 3
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) ij 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,L_2:|E| List. tr = (L_1 @ L_2) & (i:||tr||. C(Q)(i) ||L_1||i)

L_1,L_2:Trace(E). tr = (L_1 @ L_2) & L_2 = nil |E| List & (xL_1.(yL_2.(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m))
By:
Unfold `message_closure` -1
THEN
Reduce -1
THEN
ExRepD
Generated subgoal:

114. 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
L_1,L_2:Trace(E). tr = (L_1 @ L_2) & L_2 = nil & (xL_1.(yL_2.(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m))

About:
listnilassertdecidablenatural_numberapplyfunction
equalpropimpliesandallexists

(33steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc