Nuprl - mb_hybrid LEMMAs for switch_inv

Rank	Theorem	Name
8	Thm* E:TaggedEventStruct, P:TraceProperty(E). switchable(E)(P) ((switch_inv(E) No-dup-send(E)) fuses P)	[switch_inv_theorem2]
cites
0	Thm* E:Structure, P,Q_1,Q_2:((\|E\| List)Prop). (P refines Q_1) (P refines Q_2) (P refines (Q_1 Q_2))	[tr_refines_and]
7	Thm* E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) asyncR(E) preserves P delayableR(E) preserves P (P refines (Causal(E) No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P)	[switch_inv_theorem]