At: switch inv theorem3 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 P 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 Generated subgoals:
Prop
No-dup-deliver(E))
adR(E) preserves P
P:(T
R^* preserves P
R2 preserves P