---

may consider v in inning i based on knowledge (s) ==
  (ws:{a:Id| (a  A)}  List
    ((ws  W)
     (b:{a:Id| (a  A)} . ((b  ws)  ((b  dom(s))  (i = (fst(s(b)))))))
     (ws':{a:Id| (a  A)}  List
         ((ws'  W)
          (b:{a:Id| (a  A)} 
              ((b  ws)
               (b  ws')
               ((isl(snd(s(b))))  ((snd(outl(snd(s(b))))) = v))))))))
   (b:{a:Id| (a  A)} 
      ((b  dom(s))
       let j,z = s(b) in
          case z
         of inl(p) => let j',v' = p in
                        (j' = i)  (v' = v)
          | inr(x) => False))

---

Definitions :  or: P  Q,  pi1: fst(t),  all: x:A. B[x],  list: type List,  implies: P  Q,  isl: isl(x),  outl: outl(x),  pi2: snd(t),  exists: x:A. B[x],  set: {x:A| B[x]} ,  l_member: (x  l),  Id: Id,  assert: b,  fpf-dom: x  dom(f),  fpf-ap: f(x),  id-deq: IdDeq,  decide: case b of inl(x) => s[x] | inr(y) => t[y],  spread: spread def,  and: P  Q,  int: ,  equal: s = t,  false: False
FDL editor aliases :  cs-knowledge-precondition

---

may  consider  v  in  inning  i  based  on  knowledge  (s)  ==
    (\mexists{}ws:\{a:Id|  (a  \mmember{}  A)\}    List
        ((ws  \mmember{}  W)
        \mwedge{}  (\mforall{}b:\{a:Id|  (a  \mmember{}  A)\}  .  ((b  \mmember{}  ws)  {}\mRightarrow{}  ((\muparrow{}b  \mmember{}  dom(s))  \mwedge{}  (i  =  (fst(s(b)))))))
        \mwedge{}  (\mforall{}ws':\{a:Id|  (a  \mmember{}  A)\}    List
                  ((ws'  \mmember{}  W)
                  {}\mRightarrow{}  (\mexists{}b:\{a:Id|  (a  \mmember{}  A)\} 
                            ((b  \mmember{}  ws)  \mwedge{}  (b  \mmember{}  ws')  \mwedge{}  ((\muparrow{}isl(snd(s(b))))  {}\mRightarrow{}  ((snd(outl(snd(s(b)))))  =  v))))))))
    \mvee{}  (\mexists{}b:\{a:Id|  (a  \mmember{}  A)\} 
            ((\muparrow{}b  \mmember{}  dom(s))
            \mwedge{}  let  j,z  =  s(b)  in
                    case  z  of  inl(p)  =>  let  j',v'  =  p  in  (j'  =  i)  \mwedge{}  (v'  =  v)  |  inr(x)  =>  False))


Date html generated: 2010_08_27-AM-12_53_30
Last ObjectModification: 2009_12_23-PM-03_28_23

Home Index