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

At: switch decomp implies single tag decomp 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

x:||tr||. Dec(C(Q)(x))
By:
Unfold `message_closure` 0
THEN
Reduce 0
Generated subgoals:

None

About:
listnilassertdecidablenatural_numberapplyfunctionequalpropimpliesall

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