---

e@a allowed in state x ==
  (v:V
     ((e = Archive(v))
      let i,est,knw = consensus-accum-state(A;x a) in 
        ((i  fpf-domain(est)))
         may consider v in inning i based on knowledge (knw)))
   (b:{a:Id| (a  A)} . i:. z:?i  V.
       ((e = consensus-message(b;i;z))
        let i',est,knw = consensus-accum-state(A;x b) in 
          (i  i')
           case z
            of inl(p) => let j,v = p in
                           (j  dom(est))
                           (k:. ((j < k)  (k < i)  (k  dom(est))))
                           (v = est(j))
             | inr(a) => j:. ((j < i)  (j  dom(est)))))

---

Definitions :  archive-event: Archive(v),  fpf-domain: fpf-domain(f),  cs-knowledge-precondition: may consider v in inning i based on knowledge (s),  set: {x:A| B[x]} ,  l_member: (x  l),  Id: Id,  nat: ,  union: left + right,  product: x:A  B[x],  int_seg: {i..j},  natural_number: $n,  unit: Unit,  consensus-event: consensus-event(V;A),  consensus-message: consensus-message(b;i;z),  spreadn: spread3,  consensus-accum-state: consensus-accum-state(A;L),  apply: f a,  le: A  B,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  and: P  Q,  equal: s = t,  fpf-ap: f(x),  all: x:A. B[x],  int: ,  implies: P  Q,  less_than: a < b,  not: A,  assert: b,  fpf-dom: x  dom(f),  int-deq: IntDeq
FDL editor aliases :  consensus-event-constraint

---

e@a  allowed  in  state  x  ==
    (\mforall{}v:V
          ((e  =  Archive(v))
          {}\mRightarrow{}  let  i,est,knw  =  consensus-accum-state(A;x  a)  in 
                (\mneg{}(i  \mmember{}  fpf-domain(est)))  \mwedge{}  may  consider  v  in  inning  i  based  on  knowledge  (knw)))
    \mwedge{}  (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  \mforall{}i:\mBbbN{}.  \mforall{}z:?\mBbbN{}i  \mtimes{}  V.
              ((e  =  consensus-message(b;i;z))
              {}\mRightarrow{}  let  i',est,knw  =  consensus-accum-state(A;x  b)  in 
                    (i  \mleq{}  i')
                    \mwedge{}  case  z
                        of  inl(p)  =>  let  j,v  =  p  in
                                                      (\muparrow{}j  \mmember{}  dom(est))
                                                    \mwedge{}  (\mforall{}k:\mBbbZ{}.  ((j  <  k)  {}\mRightarrow{}  (k  <  i)  {}\mRightarrow{}  (\mneg{}\muparrow{}k  \mmember{}  dom(est))))
                                                    \mwedge{}  (v  =  est(j))
                          |  inr(a)  =>  \mforall{}j:\mBbbZ{}.  ((j  <  i)  {}\mRightarrow{}  (\mneg{}\muparrow{}j  \mmember{}  dom(est)))))


Date html generated: 2010_08_27-AM-12_55_45
Last ObjectModification: 2009_12_23-PM-03_31_06

Home Index