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

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

adR(E) preserves No-dup-send(E)
By:
Unfold `R_ad` 0
THEN
BackThru Thm* P:(TProp), R:(TTProp). R preserves P R^* preserves P
THEN
BackThru Thm* P:(TProp), R1,R2:(TTProp). R1 preserves P R2 preserves P R1 R2 preserves P
THEN
Try (BackThru Thm* E:EventStruct. asyncR(E) preserves No-dup-send(E))
THEN
Try (BackThru Thm* E:EventStruct. delayableR(E) preserves No-dup-send(E))
Generated subgoals:

None

About:
listapplyfunctionprop

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