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]
Thm* E:EventStruct, P:((|E| List)Prop), A:Type, evt:(A|E|), tg:(ALabel) , tr:A List. switchable(E)(P) No-dup-send(E)(map(evt;tr)) switch_inv( < A,evt,tg > (E))(tr) (m:Label. P(map(evt; < tr > _m))) P(map(evt;tr))	[switch_theorem]
Thm* E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), tr_l:A List. No-dup-send(E)(map(evt;tr_l)) No-dup-send( < A,evt,tg > (E))(tr_l)	[no_dup_send_induced]
Def full_switch_inv(E;A;evt;tg;tr_u;tr_l) == 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)	[full_switch_inv]
Def totalorder(E)(tr) == p,q:Label. agree_on_common(|MS(E)|;map(msg(E);tr delivered at p);map(msg(E);tr delivered at q))	[totalorder]

In prior sections: list 1 mb list 1 mb list 2 mb automata 1 mb structures

Try larger context: GenAutomata