At: memoryless remove msgs 2 2
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))
P(filter(
a.
(a =msg=(E) u);filter(a.reduce(b,y. (a =msg=(E) b)
y;true;v);L)))
By:
Fold `remove_msgs` 0
THEN
AllHyps
(h.
(Unfolds [`preserved_by`;`R_memoryless`] h)
THEN
(Using [`x',(L -x =msg=(E) y v)] (BackThru h)))
THEN
Reduce 0
THEN
InstConcl [u]
Generated subgoals:None
About:
