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:TaggedEventStruct, P:TraceProperty(E). switchable(E)(P) ((switch_inv(E) No-dup-send(E)) fuses P)	[switch_inv_theorem2]
Thm* E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) asyncR(E) preserves P delayableR(E) preserves P (P refines (Causal(E) No-dup-deliver(E))) ((switch_inv(E) No-dup-send(E)) fuses P)	[switch_inv_theorem]
Thm* E:TaggedEventStruct, P:TraceProperty(E). MCS(E)(P) (P refines (Causal(E) No-dup-deliver(E))) (((switch_inv(E) AD-normal(E)) No-dup-send(E)) fuses P)	[switch_inv_plus_normal]
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:TaggedEventStruct, tr:Trace(E). (switch_inv(E) No-dup-send(E))(tr) (tr':Trace(E). switch_inv(E)(tr') & AD-normal(E)(tr') & (tr adR(E) tr'))	[switch_normal_exists]
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:TaggedEventStruct, tr:|E| List, ls:||tr||. switch_inv(E)(tr) (i,j:||tr||. (i (switchR(tr)^*) ls) (j (switchR(tr)^*) ls) tag(E)(tr[i]) = tag(E)(tr[j]))	[switch_inv_rel_closure]
Thm* E:EventStruct, P:TraceProperty(E). switchable0(E)(P) switchable(E)(P Causal(E) No-dup-deliver(E))	[switchable0_switchable]
Thm* E:TaggedEventStruct, tr:|E| List. switch_inv(E)(tr) (i,j:||tr||. (i switchR(tr) j) tag(E)(tr[i]) = tag(E)(tr[j]))	[switch_inv_rel_same_tag]
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, 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:TaggedEventStruct, x:|E| List, i:(||x||-1). switch_inv(E)(x) is-send(E)(x[(i+1)]) is-send(E)(x[i]) loc(E)(x[i]) = loc(E)(x[(i+1)]) switch_inv(E)(swap(x;i;i+1))	[switch_inv_swap]
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, 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:TaggedEventStruct, P,I:TraceProperty(E). MCS(E)(P) safetyR(E) preserves I (I refines single-tag-decomposable(E)) (I fuses P)	[M_DASH_C_DASH_S_SPACE_induction]
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, 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:TaggedEventStruct, P,I:((|E| List)Prop). (P refines (Causal(E) No-dup-deliver(E))) ((I No-dup-send(E) Tag-by-msg(E) Causal(E) No-dup-deliver(E)) fuses P) ((I No-dup-send(E)) fuses P)	[no_DASH_dup_DASH_fusion]
Thm* E:TaggedEventStruct, P,I:((|E| List)Prop). (P refines Causal(E)) ((I No-dup-send(E) Tag-by-msg(E)) fuses P) ((I No-dup-send(E)) fuses P)	[tag_by_msg_fusion_lemma]
Thm* E:TaggedEventStruct, P,I,J,K:TraceProperty(E) , R:(Trace(E)Trace(E)Prop). tag_splitable(E;R) (tr_1,tr_2:Trace(E). (tr_1 R tr_2) (tr_2 R tr_1)) R preserves P R preserves K (tr:Trace(E). (I K)(tr) (tr':Trace(E). I(tr') & J(tr') & (tr R tr'))) (((I J) K) fuses P) ((I K) fuses P)	[normal_form_fusion]
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:TaggedEventStruct, I,J,P:TraceProperty(E). ((I J) fuses P) (I fuses J) (P refines J) (I fuses P)	[fusion_simplification]
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:TaggedEventStruct, I,P,Q:TraceProperty(E). (I fuses P) (I fuses Q) (I fuses (P Q))	[fusion_and]
Thm* E:TaggedEventStruct, I,J,P:TraceProperty(E). (J refines I) (I fuses P) (J fuses P)	[fusion_weakening]
Thm* E:Structure, P,Q_1,Q_2:((|E| List)Prop). (P refines Q_1) (P refines Q_2) (P refines (Q_1 Q_2))	[tr_refines_and]
Thm* E:EventStruct, L:|E| List. L = nil Causal(E)(L) (i:||L||. is-send(E)(L[i]))	[P_causal_non_nil]
Thm* E:TaggedEventStruct, tr:|E| List. (m:Label. Causal(E)( < tr > _m)) No-dup-send(E)(tr) Tag-by-msg(E)(tr)	[P_tag_by_msg_lemma]
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* msg:(AA), L1,L2:A List. (a,b:A. (a L1) (b L2) msg(a,b)) (L1 -msg(a,b) L2) = L1	[remove_msgs_disjoint]
Thm* msg:(AA), L1,L2:A List. (x:A. (x L1) (x L2)) Refl(A)(msg(_1,_2)) (L1 -msg(a,b) L2) = nil	[remove_msgs_nil]
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 switch_inv(E)(tr) == i,j,k:||tr||. i < j (is-send(E)(tr[i])) (is-send(E)(tr[j])) tag(E)(tr[i]) = tag(E)(tr[j]) tr[j] delivered at time k (k':||tr||. k' < k & tr[i] delivered at time k' & loc(E)(tr[k']) = loc(E)(tr[k]))	[switch_inv]
Def switch-decomposable(E)(L) == L = nil |E| List (Q:(||L||Prop). (i:||L||. Dec(Q(i))) & (i:||L||. Q(i)) & (i:||L||. Q(i) (is-send(E)(L[i]))) & (i,j:||L||. Q(i) Q(j) tag(E)(L[i]) = tag(E)(L[j])) & (i,j:||L||. Q(i) ij C(Q)(j)))	[switch_decomposable]
Def AD-normal(E)(tr) == i:(||tr||-1). ((is-send(E)(tr[i])) (is-send(E)(tr[(i+1)])) (tr[i] =msg=(E) tr[(i+1)])) & ((x,y:||tr||. x < y & (is-send(E)(tr[x])) & (is-send(E)(tr[y])) & tr[x] delivered at time i+1 & tr[y] delivered at time i) loc(E)(tr[i]) = loc(E)(tr[(i+1)]))	[switch_normal]
Def x somewhere delivered before y == k:||tr||. x delivered at time k & (k':||tr||. y delivered at time k' loc(E)(tr[k']) = loc(E)(tr[k]) kk')	[delivered_before_somewhere]
Def P refines Q == tr:|E| List. P(tr) Q(tr)	[tr_refines]
Def R_ad_normal(tr)(a,b) == ((is-send(E)(a)) (is-send(E)(b)) (a =msg=(E) b)) & ((is-send(E)(a)) (is-send(E)(b)) (x,y:||tr||. x < y & (is-send(E)(tr[x])) & (is-send(E)(tr[y])) & (tr[x] =msg=(E) b) & (tr[y] =msg=(E) a)) loc(E)(a) = loc(E)(b))	[R_ad_normal]
Def I fuses P == tr:Trace(E). (m:Label. P( < tr > _m)) I(tr) P(tr)	[fusion_condition]
Def single-tag-decomposable(E)(L) == L = nil |E| List (L_1,L_2:Trace(E). L = (L_1 @ L_2) |E| List & L_2 = nil |E| List & (xL_1.(yL_2.(x =msg=(E) y))) & (m:Label. (xL_2.tag(E)(x) = m)))	[single_tag_decomposable]
Def No-dup-deliver(E)(tr) == i,j:||tr||. (is-send(E)(tr[i])) (is-send(E)(tr[j])) (tr[j] =msg=(E) tr[i]) loc(E)(tr[i]) = loc(E)(tr[j]) i = j	[P_no_dup]
Def Tag-by-msg(E)(tr) == i,j:||tr||. (tr[i] =msg=(E) tr[j]) tag(E)(tr[i]) = tag(E)(tr[j])	[P_tag_by_msg]
Def switch_inv(E; tr) == i,j,k:||tr||. i < j (is-send(E)(tr[i])) (is-send(E)(tr[j])) tag(E)(tr[i]) = tag(E)(tr[j]) (tr[j] =msg=(E) tr[k]) (is-send(E)(tr[k])) (k':||tr||. k' < k & loc(E)(tr[k']) = loc(E)(tr[k]) & (tr[i] =msg=(E) tr[k']) & (is-send(E)(tr[k'])))	[switch_inv2001_03_15_DASH_PM_DASH_12_53_21]

In prior sections: core fun 1 well fnd int 1 bool 1 rel 1 sqequal 1 int 2 list 1 prog 1 mb basic mb nat union num thy 1 mb list 1 mb label mb list 2 mb collection mb tree mb automata 1 mb structures

Try larger context: GenAutomata