Nuprl Lemma : rsc4-decided

[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:]. [locs:bag(Id)]. [es:EO']. [e:E].
[i:Id]. [k:]. [v:Cmd].
  (<i, make-Msg(``rsc4 decided``;  Cmd;<k, v>)>  rsc4_Main(e)
   loc(e)  locs
       (i = loc(e))
       (e':{e':E| e' loc e } 
           a:
            (((a2:
                 b2: List
                  (<a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e')
                   ((a2 < a)  (a  b2))))
             (b:Cmd
                (<a, b>  Base([propose];  Cmd)(e')
                 (b1:. b3:Id. <<<a, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e')))))
             (((b1:
                    b2:Cmd
                     b3:Id
                      (<<<k, b1>, b2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e)
                       (a2:Cmd List
                          ((((||a2|| = (coeff * flrs))  ((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))
                           (v = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
                           (b4:Id List
                              (<a2, b4>  Memory-class(rsc4_add_to_quorum(Cmd) <a, 0>;rsc4_init() 
                                                                                      <[], []>;rsc4_vote'base(Cmd))(e)
                               ((rsc4_newvote(Cmd) <a, 0> <<<k, b1>, b2>, b3> <a2, b4>))))))))
                 ((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)))
                 ((e1:{e1:E| e1 loc e } 
                      b:
                       (((((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e1 and e))
                        (b1:
                            b2:Cmd
                             b3:Id
                              (<<<k, b1>, b2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e)
                               (a2:Cmd List
                                  ((((||a2|| = (coeff * flrs))
                                   ((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))
                                   (v = (snd(poss-maj(cmdeq;[b2 / a2];b2)))))
                                   (b4:Id List
                                      (<a2, b4>  Memory-class(rsc4_add_to_quorum(Cmd) 
                                                               <a, b>;rsc4_init() <[], []>;rsc4_vote'base(Cmd))(e)
                                       ((rsc4_newvote(Cmd) <a, b> <<<k, b1>, b2>, b3> <a2, b4>)))))))))
                        (b1:Cmd
                           (<<a, b>, b1>  Base(``rsc4 retry``;    Cmd)(e1)
                            (b5:Id. <<<a, b>, b1>, b5>  Base(``rsc4 vote``;    Cmd  Id)(e1)))))
                        (b4:
                            (b4  Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e1)
                             (b4 < b)))))
                   (no rsc4_Notify(Cmd;clients) a between e' and e))))))
Error : references
\mforall{}[Cmd:ValueAllType].  \mforall{}[clients:bag(Id)].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[coeff,flrs:\mBbbZ{}].  \mforall{}[locs:bag(Id)].
\mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].  \mforall{}[k:\mBbbZ{}].  \mforall{}[v:Cmd].
    (<i,  make-Msg(``rsc4  decided``;\mBbbZ{}  \mtimes{}  Cmd;<k,  v>)>  \mmember{}  rsc4\_Main(e)
    \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  locs
            \mwedge{}  (i  =  loc(e))
            \mwedge{}  (\mdownarrow{}\mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                      \mexists{}a:\mBbbZ{}
                        (((\mdownarrow{}\mexists{}a2:\mBbbZ{}
                                  \mexists{}b2:\mBbbZ{}  List
                                    (<a2,  b2>  \mmember{}  Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init() 
                                                                                                                                        ɘ,  []>rsc4\_Proposal(Cmd))(e')
                                    \mwedge{}  ((a2  <  a)  \mvee{}  (a  \mmember{}  b2))))
                        \mwedge{}  (\mexists{}b:Cmd
                                (<a,  b>  \mmember{}  Base([propose];\mBbbZ{}  \mtimes{}  Cmd)(e')
                                \mdownarrow{}\mvee{}  (\mexists{}b1:\mBbbZ{}.  \mexists{}b3:Id.  <<<a,  b1>,  b>,  b3>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e')))))
                        \mwedge{}  (\mdownarrow{}((\mdownarrow{}\mexists{}b1:\mBbbZ{}
                                        \mexists{}b2:Cmd
                                          \mexists{}b3:Id
                                            (<<<k,  b1>,  b2>,  b3>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e)
                                            \mwedge{}  (\mexists{}a2:Cmd  List
                                                    ((((||a2||  =  (coeff  *  flrs))
                                                    \mwedge{}  ((fst(poss-maj(cmdeq;[b2  /  a2];b2)))  =  ((coeff  *  flrs)  +  1)))
                                                    \mwedge{}  (v  =  (snd(poss-maj(cmdeq;[b2  /  a2];b2)))))
                                                    \mwedge{}  (\mexists{}b4:Id  List
                                                            (<a2,  b4>  \mmember{}  Memory-class(rsc4\_add\_to\_quorum(Cmd) 
                                                                                                              <a,  0>rsc4\_init() 
                                                                                                                            <[],  []>rsc4\_vote'base(Cmd))(e)
                                                            \mwedge{}  (\muparrow{}(rsc4\_newvote(Cmd)  <a,  0>  <<<k,  b1>,  b2>,  b3>  <a2,  b4>))))))))
                                \mwedge{}  (\mdownarrow{}(no  rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  0>  between  e'  and  e)))
                                \mvee{}  ((\mdownarrow{}\mexists{}e1:\{e1:E|  e1  \mleq{}loc  e  \} 
                                            \mexists{}b:\mBbbZ{}
                                              ((((\mdownarrow{}(no  rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  b>  between  e1  and  e))
                                              \mwedge{}  (\mdownarrow{}\mexists{}b1:\mBbbZ{}
                                                        \mexists{}b2:Cmd
                                                          \mexists{}b3:Id
                                                            (<<<k,  b1>,  b2>,  b3>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e)
                                                            \mwedge{}  (\mexists{}a2:Cmd  List
                                                                    ((((||a2||  =  (coeff  *  flrs))
                                                                    \mwedge{}  ((fst(poss-maj(cmdeq;[b2  /  a2];b2)))  =  ((coeff  *  flrs)  +  1)))
                                                                    \mwedge{}  (v  =  (snd(poss-maj(cmdeq;[b2  /  a2];b2)))))
                                                                    \mwedge{}  (\mexists{}b4:Id  List
                                                                            (<a2,  b4>  \mmember{}  Memory-class(rsc4\_add\_to\_quorum(Cmd) 
                                                                                                                              <a,  b>rsc4\_init() 
                                                                                                                                            <[],  []>rsc4\_vote'base(Cmd))(
                                                                                                    e)
                                                                            \mwedge{}  (\muparrow{}(rsc4\_newvote(Cmd)  <a,  b>  <<<k,  b1>,  b2>,  b3> 
                                                                                      <a2,  b4>)))))))))
                                              \mwedge{}  (\mexists{}b1:Cmd
                                                      (<<a,  b>,  b1>  \mmember{}  Base(``rsc4  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)(e1)
                                                      \mdownarrow{}\mvee{}  (\mexists{}b5:Id
                                                                <<<a,  b>,  b1>,  b5>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e1)))))
                                              \mwedge{}  (\mdownarrow{}\mexists{}b4:\mBbbZ{}
                                                        (b4  \mmember{}  Memory-class(rsc4\_update\_round(Cmd)  a;rsc4\_init() 
                                                                                                                                                0;rsc4\_RoundInfo(Cmd))(e1)
                                                        \mwedge{}  (b4  <  b)))))
                                    \mwedge{}  (no  rsc4\_Notify(Cmd;clients)  a  between  e'  and  e))))))


Date html generated: 2012_02_20-PM-07_51_04
Last ObjectModification: 2012_02_02-PM-02_16_21

Home Index