---

CR(in ws)[x, y]  ==
  a:{a:Id| (a  A)} 
   ((a  ws)
    (b:{a:Id| (a  A)} 
        (((b = a))
         ((Inning(y;b) = Inning(x;b))  (Estimate(y;b) = Estimate(x;b)))))
    (((Inning(y;a) = (Inning(x;a) + 1))  (Estimate(y;a) = Estimate(x;a)))
      ((Inning(y;a) = Inning(x;a))
        ((Inning(x;a)  fpf-domain(Estimate(x;a))))
        (v:V
           (state x may consider v in inning Inning(x;a)
            (Estimate(y;a) = Estimate(x;a)  Inning(x;a) : v))))))

---

Definitions :  all: x:A. B[x],  set: {x:A| B[x]} ,  implies: P  Q,  Id: Id,  or: P  Q,  add: n + m,  natural_number: $n,  not: A,  l_member: (x  l),  fpf-domain: fpf-domain(f),  exists: x:A. B[x],  and: P  Q,  cs-precondition: state s may consider v in inning i,  equal: s = t,  fpf: a:A fp-> B[a],  int: ,  fpf-join: f  g,  int-deq: IntDeq,  cs-estimate: Estimate(s;a),  fpf-single: x : v,  cs-inning: Inning(s;a)
FDL editor aliases :  consensus-rel-mod

---

CR(in  ws)[x,  y]    ==
    \mexists{}a:\{a:Id|  (a  \mmember{}  A)\} 
      ((a  \mmember{}  ws)
      \mwedge{}  (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
                ((\mneg{}(b  =  a))  {}\mRightarrow{}  ((Inning(y;b)  =  Inning(x;b))  \mwedge{}  (Estimate(y;b)  =  Estimate(x;b)))))
      \mwedge{}  (((Inning(y;a)  =  (Inning(x;a)  +  1))  \mwedge{}  (Estimate(y;a)  =  Estimate(x;a)))
          \mvee{}  ((Inning(y;a)  =  Inning(x;a))
              \mwedge{}  (\mneg{}(Inning(x;a)  \mmember{}  fpf-domain(Estimate(x;a))))
              \mwedge{}  (\mexists{}v:V
                      (state  x  may  consider  v  in  inning  Inning(x;a)
                      \mwedge{}  (Estimate(y;a)  =  Estimate(x;a)  \moplus{}  Inning(x;a)  :  v))))))


Date html generated: 2010_08_27-AM-12_48_27
Last ObjectModification: 2009_12_23-PM-03_23_53

Home Index