---

in state s, ws' blocks ws from archiving v in inning i ==
  j:
   (((0  j)  (j < i))
    (v':V
       (((v' = v))
        (b:{a:Id| (a  A)} 
            (((b  ws)  (b  ws'))
             ((j  dom(Estimate(s;b)))
                (Estimate(s;b)(j) = v')
                (k:
                    ((((j < k)  (k < i))  (k  dom(Estimate(s;b))))
                     (Estimate(s;b)(k) = v')))))))))

---

Definitions :  le: A  B,  natural_number: $n,  exists: x:A. B[x],  not: A,  set: {x:A| B[x]} ,  l_member: (x  l),  Id: Id,  all: x:A. B[x],  int: ,  implies: P  Q,  and: P  Q,  less_than: a < b,  assert: b,  fpf-dom: x  dom(f),  equal: s = t,  fpf-ap: f(x),  cs-estimate: Estimate(s;a),  int-deq: IntDeq
FDL editor aliases :  cs-archive-blocked

---

in  state  s,  ws'  blocks  ws  from  archiving  v  in  inning  i  ==
    \mexists{}j:\mBbbZ{}
      (((0  \mleq{}  j)  \mwedge{}  (j  <  i))
      \mwedge{}  (\mexists{}v':V
              ((\mneg{}(v'  =  v))
              \mwedge{}  (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\} 
                        (((b  \mmember{}  ws)  \mwedge{}  (b  \mmember{}  ws'))
                        {}\mRightarrow{}  ((\muparrow{}j  \mmember{}  dom(Estimate(s;b)))
                              \mwedge{}  (Estimate(s;b)(j)  =  v')
                              \mwedge{}  (\mforall{}k:\mBbbZ{}
                                        ((((j  <  k)  \mwedge{}  (k  <  i))  \mwedge{}  (\muparrow{}k  \mmember{}  dom(Estimate(s;b))))
                                        {}\mRightarrow{}  (Estimate(s;b)(k)  =  v')))))))))


Date html generated: 2010_08_27-AM-12_29_11
Last ObjectModification: 2009_12_23-PM-03_23_37

Home Index