send-enabledR(E)^-1 preserves No-dup-send(E) (asyncR(E) 
delayableR(E)) send-enabledR(E)^-1 preserves No-dup-send(E)
P:(T
Prop), R1,R2:(TTProp).
R1 preserves P 
R2 preserves P R1 R2 preserves P)
E:EventStruct. asyncR(E) preserves No-dup-send(E))
E:EventStruct.
delayableR(E) preserves No-dup-send(E))| 1 | send-enabledR(E)^-1 preserves No-dup-send(E) |
About:
 |