---

consensus-ts5(V;A;W) ==
  <ConsensusState  Knowledge(ConsensusState)
  , <a.<0, >, a.mk_fpf(A;b.<0, ff>)>
  , x,y.consensus-rel-knowledge(V;A;W;x;y)
  , x.v:V
        a:{a:Id| (a  A)} 
          ((Inning(fst(x);a) = 0)
           (Estimate(fst(x);a) = 0 : v)
           (Knowledge(snd(x);a) = mk_fpf(A;b.<0, ff>)))>

---

Definitions :  consensus-state4: ConsensusState,  consensus-state5: Knowledge(ConsensusState),  fpf-empty: ,  consensus-rel-knowledge: consensus-rel-knowledge(V;A;W;x;y),  exists: x:A. B[x],  all: x:A. B[x],  set: {x:A| B[x]} ,  l_member: (x  l),  cs-inning: Inning(s;a),  and: P  Q,  cs-estimate: Estimate(s;a),  pi1: fst(t),  fpf-single: x : v,  equal: s = t,  fpf: a:A fp-> B[a],  Id: Id,  union: left + right,  product: x:A  B[x],  int: ,  top: Top,  cs-knowledge: Knowledge(x;a),  pi2: snd(t),  mk_fpf: mk_fpf(L;f),  lambda: x.A[x],  pair: <a, b>,  natural_number: $n,  bfalse: ff
FDL editor aliases :  consensus-ts5

---

consensus-ts5(V;A;W)  ==
    <ConsensusState  \mtimes{}  Knowledge(ConsensusState)
    ,  <\mlambda{}a.ɘ,  \motimes{}>,  \mlambda{}a.mk\_fpf(A;\mlambda{}b.ɘ,  ff>)>
    ,  \mlambda{}x,y.consensus-rel-knowledge(V;A;W;x;y)
    ,  \mlambda{}x.\mexists{}v:V
                \mforall{}a:\{a:Id|  (a  \mmember{}  A)\} 
                    ((Inning(fst(x);a)  =  0)
                    \mwedge{}  (Estimate(fst(x);a)  =  0  :  v)
                    \mwedge{}  (Knowledge(snd(x);a)  =  mk\_fpf(A;\mlambda{}b.ɘ,  ff>)))>


Date html generated: 2010_08_27-AM-12_54_16
Last ObjectModification: 2009_12_23-PM-03_29_04

Home Index