p,q:Label. agree_on_common(|MS(E)|;map(msg(E);tr delivered at p);map(msg(E);tr delivered at q))
True
a.as' Case of bs
nil True
b.bs' 
(a 
bs) & agree_on_common(T;as';bs)
(b as) & agree_on_common(T;as;bs')
a = b T & agree_on_common(T;as';bs')
(recursive)
is mentioned by
|
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)) | [totalorder] |
In prior sections: mb list 1 mb list 2
Try larger context: GenAutomata