---

MaxVote(es;T;Vote;e;s) ==
  case s
  of inl(bv) => (e':E(Vote). ((e' <loc e)  (Vote(e') = bv)))
                 (e':E(Vote). ((e' <loc e)  ((fst(Vote(e')))  (fst(bv)))))
   | inr(x) => e':E. ((e' <loc e)  (e'  Vote))

---

Definitions :  decide: case b of inl(x) => s[x] | inr(y) => t[y],  exists: x:A. B[x],  and: P  Q,  equal: s = t,  product: x:A  B[x],  nat: ,  es-E-interface: E(X),  le: A  B,  eclass-val: X(e),  pi1: fst(t),  all: x:A. B[x],  es-E: E,  implies: P  Q,  es-locl: (e <loc e'),  not: A,  assert: b,  in-eclass: e  X
FDL editor aliases :  MaxVote

---

MaxVote(es;T;Vote;e;s)  ==
    case  s
    of  inl(bv)  =>  (\mexists{}e':E(Vote).  ((e'  <loc  e)  \mwedge{}  (Vote(e')  =  bv)))
                                \mwedge{}  (\mforall{}e':E(Vote).  ((e'  <loc  e)  {}\mRightarrow{}  ((fst(Vote(e')))  \mleq{}  (fst(bv)))))
      |  inr(x)  =>  \mforall{}e':E.  ((e'  <loc  e)  {}\mRightarrow{}  (\mneg{}\muparrow{}e'  \mmember{}\msubb{}  Vote))


Date html generated: 2010_08_28-PM-12_46_31
Last ObjectModification: 2010_04_16-AM-10_47_26

Home Index