---

in state s, inning i has committed v ==
  ws:{a:Id| (a  A)}  List
   ((ws  W)
    (a:{a:Id| (a  A)} . ((a  ws)  by state s, a archived v in inning i)))

---

Definitions :  exists: x:A. B[x],  and: P  Q,  list: type List,  all: x:A. B[x],  implies: P  Q,  set: {x:A| B[x]} ,  l_member: (x  l),  Id: Id,  cs-archived: by state s, a archived v in inning i
FDL editor aliases :  cs-inning-committed

---

in  state  s,  inning  i  has  committed  v  ==
    \mexists{}ws:\{a:Id|  (a  \mmember{}  A)\}    List
      ((ws  \mmember{}  W)  \mwedge{}  (\mforall{}a:\{a:Id|  (a  \mmember{}  A)\}  .  ((a  \mmember{}  ws)  {}\mRightarrow{}  by  state  s,  a  archived  v  in  inning  i)))


Date html generated: 2010_08_27-AM-12_49_36
Last ObjectModification: 2009_12_23-PM-03_25_21

Home Index