3. y: |E| List
4. x ((asyncR(E)
delayableR(E)) send-enabledR(E))^*^-1 y
x (((asyncR(E) delayableR(E)) send-enabledR(E)^-1)^*) y delayableR(E)) 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).
(x,y:T. (x R1 y) 
(x R2 y)) R2 preserves P R1 preserves P| 1 | 2. x: |E| List 3. y: |E| List 4. x ((asyncR(E) delayableR(E)) send-enabledR(E))^*^-1 y x (((asyncR(E) delayableR(E)) send-enabledR(E)^-1)^*) y |
About:
 |