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, 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, 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, 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* 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] |
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 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 R(tg) == swap adjacent[tg(x) = tg(y) Label]^* | [tag_rel] |
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 composableR(E)(L_1,L_2,L) == (xL_1.(yL_2.(x =msg=(E) y))) & L = (L_1 @ L_2) |E| List | [R_composable] |
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 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 x delivered at time k == (x =msg=(E) tr[k]) & (is-send(E)(tr[k])) | [delivered_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: core bool 1 rel 1 sqequal 1 int 2 list 1 prog 1 mb basic mb nat num thy 1 mb list 1 mb list 2 mb automata 1 mb structures
Try larger context: GenAutomata