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

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

safetyR(E) preserves (switch_inv(E) AD-normal(E)) No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)
By:
Repeat ((BackThru Thm* P,Q:(TProp), R:(TTProp). R preserves P R preserves Q R preserves P Q) THENA (Auto THEN (Try (Fold `trace_property` 0))))
THEN
Easy
Generated subgoals:

None

About:
listapplyfunctionprop

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