E:EventStruct. send-enabledR(E) preserves No-dup-deliver(E)as,bs:T List. ||as @ bs|| = ||as||+||bs||| Theorem | Name |
|
Thm* E:EventStruct. send-enabledR(E) preserves No-dup-deliver(E) | [P_no_dup_send_enabled] |
| cites | |
|
Thm* as,bs:T List. ||as @ bs|| = ||as||+||bs|| | [length_append] |