E:TaggedEventStruct.
(switch_inv(E) 
Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E)E:TaggedEventStruct.
(switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E))
refines single-tag-decomposable(E)
|E| List
(
Q:(
||L||
Prop).
(i:||L||. Dec(Q(i)))
& (i:||L||. Q(i))
& (i:||L||. Q(i) 
(is-send(E)(L[i])))
& (i,j:||L||. Q(i) Q(j) tag(E)(L[i]) = tag(E)(L[j]))
& (i,j:||L||. Q(i) i
j C(Q)(j)))
is mentioned by
|
Thm* E:TaggedEventStruct.
(switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E) | [strong_switch_inv_decomposable] |
|
Thm* E:TaggedEventStruct.
(switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E))
refines single-tag-decomposable(E) | [switch_decomp_implies_single_tag_decomp] |
Try larger context: GenAutomata