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, P:((|E| List)Prop), A:Type, f:(A|E|) , t:(ALabel). switchable(E)(P) switchable( < A,f,t > (E))(P o f)	[switchable_induced_tagged]
Thm* E:EventStruct. switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E))	[totalorder_switchable]
Thm* E:EventStruct, A:Type, f:(A|E|), P:((|E| List)Prop). switchable(E)(P) switchable(induced_event_str(E;A;f))(P o f)	[switchable_induced]
Thm* E:EventStruct, tr:|E| List, ls:||tr||. is-send(E)(tr[ls]) (j:||tr||. ls < j is-send(E)(tr[j])) (i,j:||tr||. ij is-send(E)(tr[j]) (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls))	[switch_inv_rel_closure_lemma1]
Thm* E:EventStruct, P:TraceProperty(E). switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E))	[switchable0_switchable]
Thm* E:EventStruct. switchable0(E)(totalorder(E))	[totalorder_switchable0]
Thm* E:EventStruct, tr:|E| List, ls,i:||tr||. is-send(E)(tr[ls]) (i (switchR(tr)^*) ls) is-send(E)(tr[i])	[switch_inv_rel_closure_send]
Thm* E:EventStruct. switchable0(E)(No-dup-deliver(E))	[P_no_dup_switchable0]
Thm* E:EventStruct. switchable0(E)(Causal(E))	[P_causal_switchable0]
Thm* E:EventStruct, P:((Label(|E| List))Prop). (f,g:(Label(|E| List)). (p:Label. g(p) f(p)) P(f) P(g)) (f,g:(Label(|E| List)). (a:|E|. p:Label. g(p) = filter(b.(b =msg=(E) a);f(p))) P(f) P(g)) (f,g,h:(Label(|E| List)). (p,q:Label. (xf(p).(yg(q).(x =msg=(E) y)))) (p:Label. h(p) = ((f(p)) @ (g(p)))) P(f) P(g) P(h)) switchable0(E)(local_deliver_property(E;P))	[local_deliver_switchable]
Thm* E:EventStruct, x:|E| List, j,z:||x||. Dec(j switchR(x) z)	[decidable__switch_inv_rel]
Thm* E:EventStruct. layerR(E)^-1 preserves No-dup-send(E)	[no_duplicate_send_layer]
Thm* E:EventStruct, x,y:|E| List. (x asyncR(E) y) (y asyncR(E) x)	[R_async_symmetric]
Thm* E:EventStruct, P:TraceProperty(E). R_permutation(E) preserves P asyncR(E) preserves P	[permutable_implies_async]
Thm* E:EventStruct. asyncR(E) preserves No-dup-send(E)	[no_duplicate_send_async]
Thm* E:EventStruct, x,y:|E| List. (x delayableR(E) y) (y delayableR(E) x)	[R_delayable_symmetric]
Thm* E:EventStruct, P:TraceProperty(E). R_permutation(E) preserves P delayableR(E) preserves P	[permutable_implies_delayable]
Thm* E:EventStruct. delayableR(E) preserves No-dup-send(E)	[no_duplicate_send_delayable]
Thm* E:EventStruct. R_permutation(E) preserves No-dup-deliver(E)	[P_no_dup_permutable]
Thm* E:EventStruct, a,b,c:|E|, tr:|E| List. a somewhere delivered before b a somewhere delivered before c c somewhere delivered before b	[delivered_before_somewhere_lemma]
Thm* E:EventStruct, a,b:|E|, tr:|E| List. a somewhere delivered before b (k:||tr||. a delivered at time k (k':||tr||. k' < k & b delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k])))	[not_delivered_before_somewhere]
Thm* E:EventStruct, tr:|E| List, x,y:|E|. Dec(x somewhere delivered before y)	[decidable__delivered_before_somewhere]
Thm* E:EventStruct, A:Type, evt:(A|E|), tg:(ALabel), m:Label , tr1,tr2:A List. (tr1 R(tg) tr2) < tr1 > _m = < tr2 > _m A List	[tag_sublist_preserved]
Thm* E:EventStruct. totalorder(E) TraceProperty(E)	[totalorder_wf]
Thm* E:EventStruct. safetyR(E) preserves No-dup-deliver(E)	[P_no_dup_deliver_safety]
Thm* E:EventStruct, P:TraceProperty(E), L,L1:|E| List. memorylessR(E) preserves P P(L) P((L -x =msg=(E) y L1))	[memoryless_remove_msgs]
Thm* E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P memorylessR(E) preserves P	[strong_safety_implies_memoryless]
Thm* E:EventStruct, P:TraceProperty(E). R_strong_safety(E) preserves P safetyR(E) preserves P	[strong_safety_implies_safety]
Thm* E:EventStruct. send-enabledR(E) preserves No-dup-deliver(E)	[P_no_dup_send_enabled]
Thm* E:EventStruct. safetyR(E) preserves Causal(E)	[P_causal_safety]
Thm* E:EventStruct. safetyR(E) preserves No-dup-send(E)	[no_duplicate_send_safety]
Thm* E:EventStruct. R_strong_safety(E) preserves No-dup-deliver(E)	[P_no_dup_strong_safety]
Thm* E:EventStruct. (ternary) composableR(E) preserves No-dup-deliver(E)	[P_no_dup_composable]
Thm* E:EventStruct, L:|E| List. L = nil Causal(E)(L) (i:||L||. is-send(E)(L[i]))	[P_causal_non_nil]
Thm* E:EventStruct, tr:|E| List. No-dup-deliver(E)(tr) (x,y:|E|. is-send(E)(x) is-send(E)(y) (y =msg=(E) x) loc(E)(x) = loc(E)(y) sublist(|E|;[x; y];tr))	[P_no_dup_iff]
Thm* E:EventStruct, tr:|E| List. Causal(E)(tr) (tr':|E| List. tr' tr (xtr'.(ytr'.is-send(E)(y) & (y =msg=(E) x))))	[P_causal_iff]
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]

In prior sections: mb structures

Try larger context: GenAutomata