At: memoryless remove msgs 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))
By:
Subst (filter(a.true;L) ~ L) 0
THEN
Try Trivial
THEN
Try
(BackThru
Thm* 
P:(T
), L:T List. (x
L.P(x)) 
(filter(P;L) ~ L))
THEN
Try ((Unfolds [`l_all`;`so_apply`] 0) THEN (Reduce 0) THEN (RW assert_pushdownC 0))
Generated subgoals:None
About:
