E:EventStruct, P:TraceProperty(E). switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E))

Unfolds [`switchable0`;`b_switchable`;`trace_property`] 0
THEN
Reduce 0
THEN
Try ((Unfolds [`tr_refines`;`prop_and`] 0) THEN (Reduce 0) THEN (Complete Auto))
THEN
Repeat (BackThru Thm* P,Q:(TProp), R:(TTProp). R preserves P R preserves Q R preserves P Q)
THEN
Repeat (BackThru Thm* P,Q:(TProp), R:(TTTProp). (ternary) R preserves P (ternary) R preserves Q (ternary) R preserves P Q )
THEN
ThinVar `P'
THEN
Inst Thm* E:EventStruct. switchable0(E)(No-dup-deliver(E)) [E]
THEN
Unfold `switchable0` -1
THEN
Reduce -1
THEN
ExRepD
THEN
Try Trivial
THEN
Inst Thm* E:EventStruct. switchable0(E)(Causal(E)) [E]
THEN
Unfold `switchable0` -1
THEN
Reduce -1
THEN
ExRepD
THEN
Try Trivial

None

About: