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

At: strong safety implies safety

E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P safetyR(E) preserves P
By:
Unfolds [`trace_property`;`preserved_by`;`R_strong_safety`;`R_safety`] 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. y x
sublist(|E|;y;x)

About:
listimpliesall

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