Nuprl - mb_hybrid Citations of totalorder

Def totalorder(E)(tr) ==

p,q:Label. agree_on_common(|MS(E)|;map(msg(E);tr delivered at p);map(msg(E);tr delivered at q))

is mentioned by

Thm* E:EventStruct. switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E)) [totalorder_switchable]

Thm* E:EventStruct. switchable0(E)(totalorder(E)) [totalorder_switchable0]

Try larger context: GenAutomata

mb hybrid Sections GenAutomata Doc

`Thm* E:EventStruct. switchable(E)(totalorder(E) Causal(E) No-dup-deliver(E))`	[totalorder_switchable]
`Thm* E:EventStruct. switchable0(E)(totalorder(E))`	[totalorder_switchable0]