---

Step * of Lemma rsc4-vote2

[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:]. [locs:bag(Id)]. [es:EO']. [e:E].
[rcvr:Id]. [num,rnd:]. [c:Cmd]. [sndr:Id].
  (<rcvr, rsc4_vote'msg(Cmd;<<<num, rnd>, c>, sndr>)>  rsc4_Main(e)
   loc(e)  locs
       (rcvr  locs  (sndr = loc(e)))
       (e':{e':E| e' loc e } 
           ((max:. missing: List. (<max, missing>  rsc4_ReplicaState(Cmd)(e')  ((max < num)  (num  missing))))
            (c':Cmd
               ((((e = e')  (c = c')  (rnd = 0))
                   ((e1:{e1:E| e1 loc e } 
                        (((maxr:. (maxr  rsc4_NewRoundsState(Cmd) num(e1)  (maxr < rnd)))
                         (<<num, rnd>, c>  rsc4_retry'base(Cmd)(e1)
                           (sndr':Id. <<<num, rnd>, c>, sndr'>  rsc4_vote'base(Cmd)(e1))))
                         (e = e1)))
                     (no rsc4_Notify(Cmd;clients) num between e' and e)))
                (<num, c'>  rsc4_propose'base(Cmd)(e')
                  (rnd':. sndr':Id. <<<num, rnd'>, c'>, sndr'>  rsc4_vote'base(Cmd)(e'))))))))
BY
{ (InstLemma `rsc4-vote` []
   THEN RepUR ``rsc4_ReplicaState rsc4_NewRoundsState rsc4_retry'base rsc4_vote'base rsc4_propose'base rsc4_vote'msg`` 0
   THEN Trivial) }

---

\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{}[rcvr:Id].  \mforall{}[num,rnd:\mBbbZ{}].  \mforall{}[c:Cmd].  \mforall{}[sndr:Id].
    (<rcvr,  rsc4\_vote'msg(Cmd;<<<num,  rnd>,  c>,  sndr>)>  \mmember{}  rsc4\_Main(e)
    \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  locs
            \mwedge{}  (rcvr  \mdownarrow{}\mmember{}  locs  \mwedge{}  (sndr  =  loc(e)))
            \mwedge{}  (\mdownarrow{}\mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                      ((\mdownarrow{}\mexists{}max:\mBbbZ{}
                              \mexists{}missing:\mBbbZ{}  List
                                (<max,  missing>  \mmember{}  rsc4\_ReplicaState(Cmd)(e')  \mwedge{}  ((max  <  num)  \mvee{}  (num  \mmember{}  missing))))
                      \mwedge{}  (\mexists{}c':Cmd
                              ((\mdownarrow{}((e  =  e')  \mwedge{}  (c  =  c')  \mwedge{}  (rnd  =  0))
                                    \mvee{}  ((\mdownarrow{}\mexists{}e1:\{e1:E|  e1  \mleq{}loc  e  \} 
                                                (((\mdownarrow{}\mexists{}maxr:\mBbbZ{}.  (maxr  \mmember{}  rsc4\_NewRoundsState(Cmd)  num(e1)  \mwedge{}  (maxr  <  rnd)))
                                                \mwedge{}  (<<num,  rnd>,  c>  \mmember{}  rsc4\_retry'base(Cmd)(e1)
                                                    \mdownarrow{}\mvee{}  (\mexists{}sndr':Id.  <<<num,  rnd>,  c>,  sndr'>  \mmember{}  rsc4\_vote'base(Cmd)(e1))))
                                                \mwedge{}  (e  =  e1)))
                                        \mwedge{}  (no  rsc4\_Notify(Cmd;clients)  num  between  e'  and  e)))
                              \mwedge{}  (<num,  c'>  \mmember{}  rsc4\_propose'base(Cmd)(e')
                                  \mdownarrow{}\mvee{}  (\mexists{}rnd':\mBbbZ{}.  \mexists{}sndr':Id.  <<<num,  rnd'>,  c'>,  sndr'>  \mmember{}  rsc4\_vote'base(Cmd)(e'))))))))


By

---

(InstLemma  `rsc4-vote`  []
  THEN  ...
  THEN  Trivial)



Home Index