Nuprl - mb_hybrid LEMMAs for P_no_dup

Theorem	Name
Thm* E:EventStruct. switchable0(E)(No-dup-deliver(E))	[P_no_dup_switchable0]
cites
Thm* E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P memorylessR(E) preserves P	[strong_safety_implies_memoryless]
Thm* E:EventStruct, P:TraceProperty(E). R_permutation(E) preserves P asyncR(E) preserves P	[permutable_implies_async]
Thm* E:EventStruct, P:TraceProperty(E). R_permutation(E) preserves P delayableR(E) preserves P	[permutable_implies_delayable]