E:EventStruct, P:TraceProperty(E), L,L1:|E| List.
memorylessR(E) preserves P 
P(L) P((L -x =msg=(E) y L1))P:(T
), L:T List. (x
L.P(x)) (filter(P;L) ~ L)| Theorem | Name |
|
Thm* E:EventStruct, P:TraceProperty(E), L,L1:|E| List.
memorylessR(E) preserves P P(L) P((L -x =msg=(E) y L1)) | [memoryless_remove_msgs] |
| cites | |
|
Thm* P:(T), L:T List. (xL.P(x)) (filter(P;L) ~ L) | [filter_trivial] |