(5steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc

At: memoryless remove msgs 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))
By: Subst (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))) 0
Generated subgoals:

1 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))
2 P(filter(a.(a =msg=(E) u);filter(a.reduce(b,y. (a =msg=(E) b)y;true;v);L)))

About:
listbtruelambdaapplyfunctionsqequalprop

(5steps) PrintForm Definitions Lemmas mb hybrid Sections GenAutomata Doc