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

At: switch inv theorem 1
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))

tag_splitable(E;adR(E))
By: Easy
Generated subgoals:

None

About:
listapplyfunctionprop

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