E:EventStruct, P:TraceProperty(E), L,L1:|E| List. memorylessR(E) preserves P P(L) P((L -x =msg=(E) y L1))

1	1. E: EventStruct 2. P: (|E| List)Prop 3. L: |E| List 4. L1: |E| List 5. memorylessR(E) preserves P 6. P(L) P(filter(x.true;L))
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(x.(x =msg=(E) u)reduce(y,y@0. (x =msg=(E) y)y@0;true;v);L))

About: