(2steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc

At: strong safety implies memoryless

E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P memorylessR(E) preserves P
By:
Unfolds [`trace_property`;`preserved_by`;`R_strong_safety`;`R_memoryless`] 0
THEN
Reduce 0
THEN
ExRepD
THEN
Using [`x',x] BackThruSomeHyp
Generated subgoal:

11. 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)

About:
listimpliesall

(2steps) PrintForm Definitions mb hybrid Sections GenAutomata Doc