Nuprl Definition : consensus-accum

consensus-accum(s;e) ==
  let i,est,knw = s in
  case e
   of inl(x) =>
   <i + 1, est, knw>
   | inr(x) =>

   case x of inl(v) => <i, est ⊕ i : v, knw> | inr(k) => let b,i',z = k in <i, est, b : <i', z> ⊕ knw>

Definitions occuring in Statement : fpf-single: x : v, fpf-join: f ⊕ g, id-deq: IdDeq, int-deq: IntDeq, spreadn: spread3, pair: <a, b>, decide: case b of inl(x) => s[x] | inr(y) => t[y], add: n + m, natural_number: $n
FDL editor aliases : consensus-accum

Latex:
consensus-accum(s;e) == let i,est,knw = s in case e of inl(x) => <i + 1, est, knw> | inr(x) => case x of inl(v) => <i, est \moplus{} i : v, knw> | inr(k) => let b,i',z = k in <i, est, b : <i', z> \moplus{} kn\000Cw> Date html generated: 2016_05_16-PM-00_28_37 Last ObjectModification: 2012_02_25-AM-11_47_35 Theory : event-ordering Home Index