Nuprl Definition : oar-consistency

Correct agents that both deliver the n-th message from a sender
agree on that message (even if it was sent by a faulty agent).⋅

oar-consistency(es;M;correct;OARDeliver) ==
  ∀e1,e2:E. ∀n:ℕ. ∀sndr:Id. ∀m1,m2:M.
    (<sndr, n, m1> ∈ OARDeliver(e1)
    ⇒ <sndr, n, m2> ∈ OARDeliver(e2)
    ⇒ (correct loc(e1))
    ⇒ (correct loc(e2))
    ⇒ (m1 = m2 ∈ M))

Definitions occuring in Statement : classrel: v ∈ X(e), es-loc: loc(e), es-E: E, Id: Id, nat: ℕ, all: ∀x:A. B[x], implies: P ⇒ Q, apply: f a, pair: <a, b>, product: x:A × B[x], equal: s = t ∈ T
FDL editor aliases : oar-consistency

Latex:
oar-consistency(es;M;correct;OARDeliver) == \mforall{}e1,e2:E. \mforall{}n:\mBbbN{}. \mforall{}sndr:Id. \mforall{}m1,m2:M. (<sndr, n, m1> \mmember{} OARDeliver(e1) {}\mRightarrow{} <sndr, n, m2> \mmember{} OARDeliver(e2) {}\mRightarrow{} (correct loc(e1)) {}\mRightarrow{} (correct loc(e2)) {}\mRightarrow{} (m1 = m2)) Date html generated: 2016_05_17-PM-03_31_22 Last ObjectModification: 2014_07_07-PM-02_11_06 Theory : event-logic-applications Home Index