---

Step * of Lemma rsc4-ilf

([Cmd:ValueAllType]. [es:EO']. [e:E].
   v:    Cmd  Id. {v  rsc4_vote'base(Cmd)(e)  v  Base(``rsc4 vote``;    Cmd  Id)(e)})
 ([a:]. [clients:bag(Id)]. [Cmd:ValueAllType]. [es:EO']. [e:E]. [i:Id]. [m:Message].
     {<i, m>  rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)|(e)
      i  clients
          (b:Cmd. ((m = make-Msg([notify];  Cmd;<a, b>))  <a, b>  Base(``rsc4 decided``;  Cmd)(e)))})
 ([a:]. [clients:bag(Id)]. [Cmd:ValueAllType]. [es:EO']. [e:E]. [i:Id]. [m:Message].
     {<i, m>  rsc4_Notify(Cmd;clients) a(e)
      (no rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)| prior to e)
          <i, m>  {rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)|}(e)})
 ([b,a,flrs,coeff:]. [Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [es:EO']. [e:E]. [i:Id]. [m:Message].
     {<i, m>  rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b>(e)
      (i = loc(e))
          (a1,b1:
              b2:Cmd
               b3:Id
                ((a2:Cmd List
                   (((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> <<<a1, b1>, b2>, b3> <a2, b4>))))
                    (((m = make-Msg(``rsc4 decided``;  Cmd;<a1, snd(poss-maj(cmdeq;[b2 / a2];b2))>))
                      ((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))
                      ((m = make-Msg(``rsc4 retry``;    Cmd;<<a1, b1 + 1>, snd(poss-maj(cmdeq;[b2 / a2];b2))>))
                        (((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1))))))
                    (||a2|| = (coeff * flrs))))
                 <<<a1, b1>, b2>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e)))})
 ([Cmd:ValueAllType]. [es:EO']. [e:E].
     v:    Cmd
       {v  rsc4_RoundInfo(Cmd)(e)
        v  Base(``rsc4 retry``;    Cmd)(e)
            (a,b:
                b1:Cmd
                 ((v = <<a, b>, b1>)  (b2:Id. <<<a, b>, b1>, b2>  Base(``rsc4 vote``;    Cmd  Id)(e))))})
 ([Cmd:ValueAllType]. [es:EO']. [e:E].
     v:  Cmd
       {v  rsc4_Proposal(Cmd)(e)
        v  Base([propose];  Cmd)(e)
            (a,b:
                b1:Cmd. ((v = <a, b1>)  (b2:Id. <<<a, b>, b1>, b2>  Base(``rsc4 vote``;    Cmd  Id)(e))))})
 ([Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:]. [locs:bag(Id)]. [es:EO'].
   [e:E]. [i:Id]. [m:Message].
     {<i, m>  rsc4_Main(e)
      loc(e)  locs
          (e':{e':E| e' loc e } 
              a:
               ((b:Cmd
                  ((<a, b>  Base([propose];  Cmd)(e')
                   (b1:. b3:Id. <<<a, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e')))
                   (((((i  locs  (m = make-Msg(``rsc4 vote``;    Cmd  Id;<<<a, 0>, b>, loc(e)>)))  (e = e'))
                     ((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)
                        <i, m>  {rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0>}(e)))
                     ((no rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)| between e' and e)
                       <i, m>  {rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)|}(e)))
                     ((no rsc4_Notify(Cmd;clients) a between e' and e)
                        (e1:{e1:E| e1 loc e } 
                            b:
                             ((b1:Cmd
                                ((((i  locs  (m = make-Msg(``rsc4 vote``;    Cmd  Id;<<<a, b>, b1>, loc(e)>)))
                                 (e = e1))
                                 ((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b> between e1 and e)
                                    <i, m>  {rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b>}(e)))
                                 (<<a, b>, b1>  Base(``rsc4 retry``;    Cmd)(e1)
                                   (b5:Id. <<..., ...>, ...>  ...(...)))))
                              ...))))))
                ...))})
BY
{ (InstLemma `rsc4-ilf-hide` [] THEN All (Unfold `hide`) THEN Trivial) }

---

(\mforall{}[Cmd:ValueAllType].  \mforall{}[es:EO'].  \mforall{}[e:E].
      \mforall{}v:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id
          \{v  \mmember{}  rsc4\_vote'base(Cmd)(e)  \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e)\})
\mwedge{}  (\mforall{}[a:\mBbbZ{}].  \mforall{}[clients:bag(Id)].  \mforall{}[Cmd:ValueAllType].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].  \mforall{}[m:Message].
          \{<i,  m>  \mmember{}  rsc4\_decision(Cmd;clients)  a@|Loc,  rsc4\_decided'base(Cmd)|(e)
          \mLeftarrow{}{}\mRightarrow{}  i  \mdownarrow{}\mmember{}  clients
                  \mwedge{}  (\mdownarrow{}\mexists{}b:Cmd
                            ((m  =  make-Msg([notify];\mBbbZ{}  \mtimes{}  Cmd;<a,  b>))
                            \mwedge{}  <a,  b>  \mmember{}  Base(``rsc4  decided``;\mBbbZ{}  \mtimes{}  Cmd)(e)))\})
\mwedge{}  (\mforall{}[a:\mBbbZ{}].  \mforall{}[clients:bag(Id)].  \mforall{}[Cmd:ValueAllType].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].  \mforall{}[m:Message].
          \{<i,  m>  \mmember{}  rsc4\_Notify(Cmd;clients)  a(e)
          \mLeftarrow{}{}\mRightarrow{}  (no  rsc4\_decision(Cmd;clients)  a@|Loc,  rsc4\_decided'base(Cmd)|  prior  to  e)
                  \mwedge{}  <i,  m>  \mmember{}  \{rsc4\_decision(Cmd;clients)  a@|Loc,  rsc4\_decided'base(Cmd)|\}(e)\})
\mwedge{}  (\mforall{}[b,a,flrs,coeff:\mBbbZ{}].  \mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[es:EO'].  \mforall{}[e:E].  \mforall{}[i:Id].
      \mforall{}[m:Message].
          \{<i,  m>  \mmember{}  rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  b>(e)
          \mLeftarrow{}{}\mRightarrow{}  (i  =  loc(e))
                  \mwedge{}  (\mdownarrow{}\mexists{}a1,b1:\mBbbZ{}
                            \mexists{}b2:Cmd
                              \mexists{}b3:Id
                                ((\mexists{}a2:Cmd  List
                                      (((\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>  <<<a1,  b1>,  b2>,  b3>  <a2,  b4>))))
                                      \mwedge{}  (((m
                                          =  make-Msg(``rsc4  decided``;\mBbbZ{}  \mtimes{}  Cmd;<a1,  snd(poss-maj(cmdeq;[b2  /  a2];b2))>))
                                          \mwedge{}  ((fst(poss-maj(cmdeq;[b2  /  a2];b2)))  =  ((coeff  *  flrs)  +  1)))
                                          \mvee{}  ((m
                                              =  make-Msg(``rsc4  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd;<<a1,  b1  +  1>
                                                  ,  snd(poss-maj(cmdeq;[b2  /  a2];b2))
                                                  >))
                                              \mwedge{}  (\mneg{}((fst(poss-maj(cmdeq;[b2  /  a2];b2)))  =  ((coeff  *  flrs)  +  1))))))
                                      \mwedge{}  (||a2||  =  (coeff  *  flrs))))
                                \mwedge{}  <<<a1,  b1>,  b2>,  b3>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e)))\})
\mwedge{}  (\mforall{}[Cmd:ValueAllType].  \mforall{}[es:EO'].  \mforall{}[e:E].
          \mforall{}v:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd
              \{v  \mmember{}  rsc4\_RoundInfo(Cmd)(e)
              \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  Base(``rsc4  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)(e)
                      \mdownarrow{}\mvee{}  (\mexists{}a,b:\mBbbZ{}
                                \mexists{}b1:Cmd
                                  ((v  =  <<a,  b>,  b1>)
                                  \mwedge{}  (\mexists{}b2:Id.  <<<a,  b>,  b1>,  b2>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e))))\})
\mwedge{}  (\mforall{}[Cmd:ValueAllType].  \mforall{}[es:EO'].  \mforall{}[e:E].
          \mforall{}v:\mBbbZ{}  \mtimes{}  Cmd
              \{v  \mmember{}  rsc4\_Proposal(Cmd)(e)
              \mLeftarrow{}{}\mRightarrow{}  v  \mmember{}  Base([propose];\mBbbZ{}  \mtimes{}  Cmd)(e)
                      \mdownarrow{}\mvee{}  (\mexists{}a,b:\mBbbZ{}
                                \mexists{}b1:Cmd
                                  ((v  =  <a,  b1>)
                                  \mwedge{}  (\mexists{}b2:Id.  <<<a,  b>,  b1>,  b2>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e))))\})
\mwedge{}  (\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{}[m:Message].
          \{<i,  m>  \mmember{}  rsc4\_Main(e)
          \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  locs
                  \mwedge{}  (\mdownarrow{}\mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                            \mexists{}a:\mBbbZ{}
                              ((\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{}  (((((i  \mdownarrow{}\mmember{}  locs
                                        \mwedge{}  (m  =  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<a,  0>,  b>,  loc(e)>)))
                                        \mwedge{}  (e  =  e'))
                                        \mdownarrow{}\mvee{}  ((no  rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  0>  between  e'  and  e)
                                              \mwedge{}  <i,  m>  \mmember{}  \{rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  0>\}(e)))
                                        \mvee{}  ((no  rsc4\_decision(Cmd;clients) 
                                                      a@|Loc,  rsc4\_decided'base(Cmd)|  between  e'  and  e)
                                            \mwedge{}  <i,  m>  \mmember{}  \{rsc4\_decision(Cmd;clients)  a@|Loc,  rsc4\_decided'base(Cmd)|\}(e)))
                                        \mdownarrow{}\mvee{}  ((no  rsc4\_Notify(Cmd;clients)  a  between  e'  and  e)
                                              \mwedge{}  (\mdownarrow{}\mexists{}e1:\{e1:E|  e1  \mleq{}loc  e  \} 
                                                        \mexists{}b:\mBbbZ{}
                                                          ((\mexists{}b1:Cmd
                                                                ((((i  \mdownarrow{}\mmember{}  locs
                                                                \mwedge{}  (m
                                                                    =  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<a,  b>,  b1>
                                                                        ,  loc(e)
                                                                        >)))
                                                                \mwedge{}  (e  =  e1))
                                                                \mdownarrow{}\mvee{}  ((no  rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  b>  between  e1  and  e)
                                                                      \mwedge{}  <i,  m>  \mmember{}  \{rsc4\_Quorum(Cmd;cmdeq;coeff;flrs)  <a,  b>\}(e)))
                                                                \mwedge{}  (<<a,  b>,  b1>  \mmember{}  Base(``rsc4  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)(e1)
                                                                    \mdownarrow{}\mvee{}  (\mexists{}b5:Id.  <<...,  ...>,  ...>  \mmember{}  ...(...)))))
                                                          \mwedge{}  ...))))))
                              \mwedge{}  ...))\})


By

---

(InstLemma  `rsc4-ilf-hide`  []  THEN  All  (Unfold  `hide`)  THEN  Trivial)



Home Index