E:EventStruct, P:TraceProperty(E), A:Type, evt:(A
|E|)
, tg:(ALabel), tr_u:Trace(E), tr_l:A List.
switchable(E)(P) 
No-dup-send(E)(tr_u)
full_switch_inv(E;A;evt;tg;tr_u;tr_l) (m:Label. P(map(evt; < tr_l > _m))) P(tr_u)
tr_m:A List.
(tr_l R(tg) tr_m) & (map(evt;tr_m) layerR(E) tr_u) & switch_inv( < A,evt,tg > (E))(tr_m)
is mentioned by
|
Thm* E:EventStruct, P:TraceProperty(E), A:Type, evt:(A|E|)
, tg:(ALabel), tr_u:Trace(E), tr_l:A List.
switchable(E)(P)
No-dup-send(E)(tr_u)
full_switch_inv(E;A;evt;tg;tr_u;tr_l) (m:Label. P(map(evt; < tr_l > _m))) P(tr_u) | [switch_main_theorem] |
Try larger context: GenAutomata