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

At: switch inv plus normal 1 2
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)) refines single-tag-decomposable(E)
By:
Inst Thm* E:TaggedEventStruct. (switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E) [E]
THEN
Inst Thm* E:TaggedEventStruct. (switch-decomposable(E) Tag-by-msg(E) Causal(E) No-dup-send(E)) refines single-tag-decomposable(E) [E]
THEN
All (Unfold `tr_refines`)
THEN
Try (Fold `trace_property` 0)
THEN
BackThruSomeHyp
THEN
All (h.(Unfold `prop_and` h) THEN (Reduce h))
THEN
EasyHyp
Generated subgoals:

None

About:
listapplyfunctionprop

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