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

At: switch decomp implies single tag decomp 3 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) 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: |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))
By: Assert (||tr|| = ||L_1||+||L_2||)
Generated subgoals:

1 ||tr|| = ||L_1||+||L_2||
218. ||tr|| = ||L_1||+||L_2||
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:
listnilassertdecidableintnatural_numberaddapplyfunction
equalpropimpliesandallexists

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