---

Step * of Lemma rsc4-notify

[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([notify];  Cmd;<k, v>)>  rsc4_Main(e)
   loc(e)  locs
       (<k, v>  Base(``rsc4 decided``;  Cmd)(e)  i  clients)
       (e':{e':E| e' loc e } 
           (((a2:
                b2: List
                 (<a2, b2>  Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e')
                  ((a2 < k)  (k  b2))))
            (b:Cmd
               (<k, b>  Base([propose];  Cmd)(e')
                (b1:. b3:Id. <<<k, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e')))))
            ((no rsc4_decision(Cmd;clients) k@|Loc, rsc4_decided'base(Cmd)| between e' and e)))))
BY
{ ProveILF_instance "notify""rsc4" }

---

\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([notify];\mBbbZ{}  \mtimes{}  Cmd;<k,  v>)>  \mmember{}  rsc4\_Main(e)
    \mLeftarrow{}{}\mRightarrow{}  loc(e)  \mdownarrow{}\mmember{}  locs
            \mwedge{}  (<k,  v>  \mmember{}  Base(``rsc4  decided``;\mBbbZ{}  \mtimes{}  Cmd)(e)  \mwedge{}  i  \mdownarrow{}\mmember{}  clients)
            \mwedge{}  (\mdownarrow{}\mexists{}e':\{e':E|  e'  \mleq{}loc  e  \} 
                      (((\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  <  k)  \mvee{}  (k  \mmember{}  b2))))
                      \mwedge{}  (\mexists{}b:Cmd
                              (<k,  b>  \mmember{}  Base([propose];\mBbbZ{}  \mtimes{}  Cmd)(e')
                              \mdownarrow{}\mvee{}  (\mexists{}b1:\mBbbZ{}.  \mexists{}b3:Id.  <<<k,  b1>,  b>,  b3>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e')))))
                      \mwedge{}  (\mdownarrow{}(no  rsc4\_decision(Cmd;clients)  k@|Loc,  rsc4\_decided'base(Cmd)|  between  e'  and  e)))))


By

---

ProveILF\_instance  "notify""rsc4"



Home Index