At: strong safety implies memoryless 1
1. E: EventStruct
2. P: (|E| List)
Prop
3. 
x,y:|E| List. P(x) 
sublist(|E|;y;x) P(y)
4. x: |E| List
5. y: |E| List
6. P(x)
7. a: |E|
8. y = filter(
b.
(b =msg=(E) a);x)
sublist(|E|;y;x)
By:
HypSubst -1 0
THEN
Easy
Generated subgoals:None
About:
