is mentioned by

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, 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: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, 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]
Def switchR(tr)(i,j) == (is-send(E)(tr[i])) & (is-send(E)(tr[j])) & i < j & tr[j] somewhere delivered before tr[i] j < i & tr[i] somewhere delivered before tr[j]	[switch_inv_rel]
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 asyncR(E) == swap adjacent[loc(E)(x) = loc(E)(y) & (is-send(E)(x)) & (is-send(E)(y)) (is-send(E)(x)) & (is-send(E)(y))]	[R_async]
Def delayableR(E) == swap adjacent[(x =msg=(E) y) & (is-send(E)(x)) & (is-send(E)(y)) (is-send(E)(x)) & (is-send(E)(y))]	[R_delayable]
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 Macro x R_del(E) y == (x =msg=(E) y) & is-deliver(E)(x) & (is-send(E)(y)) (is-send(E)(x)) & is-deliver(E)(y)	[R_del]
Def send-enabledR(E)(L_1,L_2) == x:|E|. (is-send(E)(x)) & L_2 = (L_1 @ [x])	[R_send_enabled]
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 Causal(E)(tr) == i:||tr||. j:||tr||. ji & (is-send(E)(tr[j])) & (tr[j] =msg=(E) tr[i])	[P_causal]
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 x delivered at time k == (x =msg=(E) tr[k]) & (is-send(E)(tr[k]))	[delivered_at]
Def tr delivered at p == filter(e.is-send(E)(e)loc(E)(e) = p;tr)	[deliveries_at]
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: mb structures

Try larger context: GenAutomata