---

in state s, inning i could commit 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
            in state s, a has not completed 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,  or: P  Q,  cs-archived: by state s, a archived v in inning i,  cs-not-completed: in state s, a has not completed inning i
FDL editor aliases :  cs-inning-committable

---

in  state  s,  inning  i  could  commit  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  \mvee{}  in  state  s,  a  has  not  completed  inning  i))))


Date html generated: 2010_08_27-AM-12_49_46
Last ObjectModification: 2009_12_23-PM-03_25_32

Home Index