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

At: switch inv theorem 6
1. E: TaggedEventStruct
2. P: (|E| List)Prop
3. MCS(E)(P)
4. asyncR(E) preserves P
5. delayableR(E) preserves P
6. P refines (Causal(E) No-dup-deliver(E))

((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P
By:
Inst Thm* E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) (P refines (Causal(E) No-dup-deliver(E))) (((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P) [E;P]
THEN
Auto
THEN
Try (Unfold `trace_property` 0)
Generated subgoals:

None

About:
listapplyfunctionprop

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