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

At: switch inv plus normal 1
1. E: TaggedEventStruct
2. P: (|E| List)Prop
3. MCS(E)(P)
4. P refines (Causal(E) No-dup-deliver(E))

((switch_inv(E) AD-normal(E)) No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P
By:
BackThru `M-C-S induction`
THEN
Try (Unfold `trace_property` 0)
THEN
Try (Fold `trace_property` 0)
Generated subgoals:

1 safetyR(E) preserves (switch_inv(E) AD-normal(E)) No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)
2 ((switch_inv(E) AD-normal(E)) No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) refines single-tag-decomposable(E)

About:
listapplyfunctionprop

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