Nuprl Lemma : RSC_progress

[Cmd:ValueAllType]. [eq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [f:]. [es:EO'].
  ((RSC_SimpleConsensus_stdma{mark-simple-consensus-V2.esh:o, i:l}(Cmd; clients; eq; f; locs) es)
   (e:E
        (loc(e)  locs
         (n:. c:Cmd.
              (<n, c>  RSC_Propose(Cmd)(e)
               (r:
                    ((e:E. c:Cmd. <n, c>  RSC_Decided(Cmd)(e))
                       (i,j:{i:Id| i  locs} .
                           (i  locs  (e:E. ((loc(e) = j)  (c:Cmd. <<<n, r>, c>, i>  RSC_Vote(Cmd)(e)))))))))))))


Proof not projected

Error : references
\mforall{}[Cmd:ValueAllType].  \mforall{}[eq:EqDecider(Cmd)].  \mforall{}[locs,clients:bag(Id)].  \mforall{}[f:\mBbbZ{}].  \mforall{}[es:EO'].
    ((RSC\_SimpleConsensus\_stdma\{mark-simple-consensus-V2.esh:o,  i:l\}(Cmd;  clients;  eq;  f;  locs)  es)
    {}\mRightarrow{}  (\mforall{}e:E
                (loc(e)  \mdownarrow{}\mmember{}  locs
                {}\mRightarrow{}  (\mforall{}n:\mBbbZ{}.  \mforall{}c:Cmd.
                            (<n,  c>  \mmember{}  RSC\_Propose(Cmd)(e)
                            {}\mRightarrow{}  (\mforall{}r:\mBbbN{}
                                        (\mdownarrow{}(\mexists{}e:E.  \mexists{}c:Cmd.  <n,  c>  \mmember{}  RSC\_Decided(Cmd)(e))
                                            \mvee{}  (\mforall{}i,j:\{i:Id|  i  \mdownarrow{}\mmember{}  locs\}  .
                                                      (i  \mdownarrow{}\mmember{}  locs
                                                      {}\mRightarrow{}  (\mexists{}e:E
                                                                ((loc(e)  =  j)
                                                                \mwedge{}  (\mexists{}c:Cmd.  <<<n,  r>,  c>,  i>  \mmember{}  RSC\_Vote(Cmd)(e)))))))))))))


Date html generated: 2012_02_20-PM-07_51_00
Last ObjectModification: 2012_02_02-PM-01_59_55

Home Index