At: memoryless remove msgs21 1. E: EventStruct 2. P: (|E| List)Prop 3. L: |E| List 4. L1: |E| List 5. memorylessR(E) preserves P 6. P(L) 7. u: |E| 8. v: |E| List 9. P((L -x =msg=(E) y v))
filter(a.(a =msg=(E) u)reduce(b,y. (a =msg=(E) b)y;true;v);L) ~ filter(a.
(a =msg=(E) u);filter(a.reduce(b,y. (a =msg=(E) b)y;true;v);L)) By: RW FilterFilterC 0
THEN
Reduce 0
THEN
Trivial Generated subgoals:
Prop
filter(
a.
(a =msg=(E) u)