Nuprl Definition : oar-order

A correct orderer ⌈x ↓∈ orderers⌉ signs ⌈<sndr, n, msg>⌉ only if it has
previously signed messages ⌈<sndr, n', msg'>⌉ for all n' < n, and
it has never previously signed ⌈<sndr, n, msg>⌉, and
it does not simultaneously sign any other msg for sequence number n
and sender sndr.⋅

oar-order(es;M;S;correct;orderers) ==
  ∀n:ℕ. ∀sndr:Id. ∀msg:M. ∀sig:Atom1. ∀x:Id. ∀e:E.
    ((x ↓∈ orderers ∧ <x, sig, sndr, n, msg> ∈ S(e) ∧ (correct x))
    ⇒ ((0 < n ⇒ (∃msg':M. ∃sig':Atom1. ∃e':E. ((e' <loc e) ∧ <x, sig', sndr, n - 1, msg'> ∈ S(e'))))
       ∧ (∀msg':M. ∀sig':Atom1. ∀e':E.  ((e' <loc e) ⇒ (¬<x, sig', sndr, n, msg'> ∈ S(e'))))
       ∧ (∀msg':M. ∀sig':Atom1.  (<x, sig', sndr, n, msg'> ∈ S(e) ⇒ (msg' = msg ∈ M)))))

Definitions occuring in Statement : classrel: v ∈ X(e), es-locl: (e <loc e'), es-E: E, Id: Id, nat: ℕ, atom: Atom$n, less_than: a < b, all: ∀x:A. B[x], exists: ∃x:A. B[x], not: ¬A, implies: P ⇒ Q, and: P ∧ Q, apply: f a, pair: <a, b>, product: x:A × B[x], subtract: n - m, natural_number: $n, equal: s = t ∈ T, bag-member: x ↓∈ bs
FDL editor aliases : oar-order

Latex:
oar-order(es;M;S;correct;orderers) == \mforall{}n:\mBbbN{}. \mforall{}sndr:Id. \mforall{}msg:M. \mforall{}sig:Atom1. \mforall{}x:Id. \mforall{}e:E. ((x \mdownarrow{}\mmember{} orderers \mwedge{} <x, sig, sndr, n, msg> \mmember{} S(e) \mwedge{} (correct x)) {}\mRightarrow{} ((0 < n {}\mRightarrow{} (\mexists{}msg':M. \mexists{}sig':Atom1. \mexists{}e':E. ((e' <loc e) \mwedge{} <x, sig', sndr, n - 1, msg'> \mmember{} S(e')))) \mwedge{} (\mforall{}msg':M. \mforall{}sig':Atom1. \mforall{}e':E. ((e' <loc e) {}\mRightarrow{} (\mneg{}<x, sig', sndr, n, msg'> \mmember{} S(e')))) \mwedge{} (\mforall{}msg':M. \mforall{}sig':Atom1. (<x, sig', sndr, n, msg'> \mmember{} S(e) {}\mRightarrow{} (msg' = msg))))) Date html generated: 2015_07_23-PM-00_26_53 Last ObjectModification: 2014_07_07-PM-02_06_59 Home Index