Nuprl Lemma : RSC_vote

[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [flrs:]. [locs:bag(Id)]. [es:EO']. [e:E].
[i:Id]. [k,k1:]. [v:Cmd]. [i1:Id].
  (<i, make-Msg(``sc vote``;    Cmd  Id;<<<k, k1>, v>, i1>)>  RSC_main(Cmd;clients;cmdeq;flrs;locs)(e)
   loc(e)  locs
       i  locs
       (i1 = loc(e))
       (e':{e':E| e' loc e } 
           z:
            z1:Cmd
             (((<z, z1>  Base(``sc propose``;  Cmd)(e')
              (a3:. a5:Id. <<<z, a3>, z1>, a5>  Base(``sc vote``;    Cmd  Id)(e')))
              (b:
                  b1: List
                   (<b, b1>  Prior(Accum-class(v,state.
                                                 if RSC_new_proposal() v state
                                                 then RSC_onnewpropose() v state
                                                 else state
                                                 fi ;RSC_init() <0, []>;RSC_Proposal(Cmd)))?RSC_init() <0, []>(e')
                    ((RSC_new_proposal() <z, z1> <b, b1>)))))
              (((k = z)  (k1 = 0)  (v = z1)  (e = e'))
                  ((no RSC_Notify(Cmd;clients) z between e' and e)
                    (b:{x:| x = 0} 
                        (b  Prior(Accum-class(v,state.
                                                if RSC_round_increase() z v state
                                                then RSC_incround() v state
                                                else state
                                                fi ;RSC_init() 0;RSC_RoundInfo(Cmd)))?RSC_init() 0(e)
                         ((RSC_round_increase() z <<k, k1>, v> b))))
                    (<<k, k1>, v>  Base(``sc retry``;    Cmd)(e)
                      (a6:Id. <<<k, k1>, v>, a6>  Base(``sc vote``;    Cmd  Id)(e))))))))


Proof not projected

Error : references
\mforall{}[Cmd:ValueAllType].  \mforall{}[clients:bag(Id)].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[flrs:\mBbbZ{}].  \mforall{}[locs:bag(Id)].
\mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].  \mforall{}[k,k1:\mBbbZ{}].  \mforall{}[v:Cmd].  \mforall{}[i1:Id].
    (<i,  make-Msg(``sc  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<k,  k1>,  v>,  i1>)>  \mmember{}
        RSC\_main(Cmd;clients;cmdeq;flrs;locs)(e)
    \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  locs
            \mwedge{}  i  \mdownarrow{}\mmember{}  locs
            \mwedge{}  (i1  =  loc(e))
            \mwedge{}  (\mdownarrow{}\mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                      \mexists{}z:\mBbbZ{}
                        \mexists{}z1:Cmd
                          (((<z,  z1>  \mmember{}  Base(``sc  propose``;\mBbbZ{}  \mtimes{}  Cmd)(e')
                          \mdownarrow{}\mvee{}  (\mexists{}a3:\mBbbZ{}.  \mexists{}a5:Id.  <<<z,  a3>,  z1>,  a5>  \mmember{}  Base(``sc  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e')))
                          \mwedge{}  (\mdownarrow{}\mexists{}b:\mBbbZ{}
                                    \mexists{}b1:\mBbbZ{}  List
                                      (<b,  b1>  \mmember{}  Prior(Accum-class(\mlambda{}v,state.
                                                                                                  if  RSC\_new\_proposal()  v  state
                                                                                                  then  RSC\_onnewpropose()  v  state
                                                                                                  else  state
                                                                                                  fi  ;RSC\_init() 
                                                                                                          ɘ,  []>RSC\_Proposal(Cmd)))?RSC\_init()  ɘ,  []>(
                                                            e')
                                      \mwedge{}  (\muparrow{}(RSC\_new\_proposal()  <z,  z1>  <b,  b1>)))))
                          \mwedge{}  (\mdownarrow{}((k  =  z)  \mwedge{}  (k1  =  0)  \mwedge{}  (v  =  z1)  \mwedge{}  (e  =  e'))
                                  \mvee{}  ((no  RSC\_Notify(Cmd;clients)  z  between  e'  and  e)
                                      \mwedge{}  (\mdownarrow{}\mexists{}b:\{x:\mBbbZ{}|  x  =  0\} 
                                                (b  \mmember{}  Prior(Accum-class(\mlambda{}v,state.
                                                                                                if  RSC\_round\_increase()  z  v  state
                                                                                                then  RSC\_incround()  v  state
                                                                                                else  state
                                                                                                fi  ;RSC\_init()  0;RSC\_RoundInfo(Cmd)))?RSC\_init()  0(
                                                          e)
                                                \mwedge{}  (\muparrow{}(RSC\_round\_increase()  z  <<k,  k1>,  v>  b))))
                                      \mwedge{}  (<<k,  k1>,  v>  \mmember{}  Base(``sc  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)(e)
                                          \mdownarrow{}\mvee{}  (\mexists{}a6:Id.  <<<k,  k1>,  v>,  a6>  \mmember{}  Base(``sc  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e))))))))


Date html generated: 2012_02_20-PM-07_50_57
Last ObjectModification: 2012_02_02-PM-01_59_19

Home Index