mb hybrid Sections GenAutomata Doc

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)]))

is mentioned by

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: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:TaggedEventStruct. (switch_inv(E) Causal(E) AD-normal(E) No-dup-deliver(E)) refines switch-decomposable(E)[strong_switch_inv_decomposable]
Thm* E:TaggedEventStruct. safetyR(E) preserves AD-normal(E)[switch_normal_safety]

Try larger context: GenAutomata

mb hybrid Sections GenAutomata Doc