---

Step * of Lemma rsc4-vote

[Cmd:ValueAllType]. [clients:bag(Id)]. [cmdeq:EqDecider(Cmd)]. [coeff,flrs:]. [locs:bag(Id)]. [es:EO']. [e:E].
[i:Id]. [k,k1:]. [v:Cmd]. [i1:Id].
  (<i, make-Msg(``rsc4 vote``;    Cmd  Id;<<<k, k1>, v>, i1>)>  rsc4_Main(e)
   loc(e)  locs
       (i  locs  (i1 = loc(e)))
       (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
               ((((e = e')  (v = b)  (k1 = 0))
                   ((e1:{e1:E| e1 loc e } 
                        (((b4:
                             (b4  Memory-class(rsc4_update_round(Cmd) k;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e1)
                              (b4 < k1)))
                         (<<k, k1>, v>  Base(``rsc4 retry``;    Cmd)(e1)
                           (b5:Id. <<<k, k1>, v>, b5>  Base(``rsc4 vote``;    Cmd  Id)(e1))))
                         (e = e1)))
                     (no rsc4_Notify(Cmd;clients) k between e' and e)))
                (<k, b>  Base([propose];  Cmd)(e')
                  (b1:. b3:Id. <<<k, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e'))))))))
BY
{ ProveILF_instance "vote""rsc4" }

1
.....failed RWconcl..... 
1. Cmd : {T:Type| valueall-type(T)} 
2. clients : bag(Id)
3. cmdeq : EqDecider(Cmd)
4. coeff : 
5. flrs : 
6. locs : bag(Id)
7. es : EO'
8. e : E
9. i : Id
10. k : 
11. k1 : 
12. v : Cmd
13. i1 : Id
14. loc(e)  locs  loc(e)  locs
15. e' : {e':E| e' loc e } 
16. a : 
17. b : Cmd
18. <a, b>  Base([propose];  Cmd)(e')
     (b1:. b3:Id. <<<a, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e'))
 <a, b>  Base([propose];  Cmd)(e')
     (b1:. b3:Id. <<<a, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e'))
19. (((i  locs  (((k = a)  (k1 = 0))  (v = b))  (i1 = loc(e)))  (e = e'))
     ((no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, 0> between e' and e)
        (i = loc(e))
        (a1:
            (False
             (b1:
                b2:Cmd
                 b3:Id
                  (<<<a1, 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))
                         (((fst(poss-maj(cmdeq;[b2 / a2];b2))) = ((coeff * flrs) + 1)))))
                       (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> <<<a1, b1>, b2>, b3> <a2, b4>))))))))))))
     False
 (((i  locs
     (make-Msg(``rsc4 vote``;    Cmd  Id;<<<k, k1>, v>, i1>)
      = 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, make-Msg(``rsc4 vote``;    Cmd  Id;<<<k, k1>, v>, i1>)> 
          {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, make-Msg(``rsc4 vote``;    Cmd  Id;<<<k, k1>, v>, i1>)> 
         {rsc4_decision(Cmd;clients) a@|Loc, rsc4_decided'base(Cmd)|}(e))
20. (no rsc4_Notify(Cmd;clients) a between e' and e)  (no rsc4_Notify(Cmd;clients) a between e' and e)
21. e1 : {e1:E| e1 loc e } 
22. b1 : 
23. b1@0 : Cmd
24. i  locs  i  locs
25. (((k = a)  (k1 = b1))  (v = b1@0))  (i1 = loc(e))  '
26. <<<k, k1>, v>, i1> = <<<a, b1>, b1@0>, loc(e)>  '
27. (((k = a)  (k1 = b1))  (v = b1@0))  (i1 = loc(e))
 <<<k, k1>, v>, i1> = <<<a, b1>, b1@0>, loc(e)>

---

\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,k1:\mBbbZ{}].  \mforall{}[v:Cmd].  \mforall{}[i1:Id].
    (<i,  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<k,  k1>,  v>,  i1>)>  \mmember{}  rsc4\_Main(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  \} 
                      ((\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
                              ((\mdownarrow{}((e  =  e')  \mwedge{}  (v  =  b)  \mwedge{}  (k1  =  0))
                                    \mvee{}  ((\mdownarrow{}\mexists{}e1:\{e1:E|  e1  \mleq{}loc  e  \} 
                                                (((\mdownarrow{}\mexists{}b4:\mBbbZ{}
                                                          (b4  \mmember{}  Memory-class(rsc4\_update\_round(Cmd)  k;rsc4\_init() 
                                                                                                                                                  0;rsc4\_RoundInfo(Cmd))(e1)
                                                          \mwedge{}  (b4  <  k1)))
                                                \mwedge{}  (<<k,  k1>,  v>  \mmember{}  Base(``rsc4  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)(e1)
                                                    \mdownarrow{}\mvee{}  (\mexists{}b5:Id
                                                              <<<k,  k1>,  v>,  b5>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e1))))
                                                \mwedge{}  (e  =  e1)))
                                        \mwedge{}  (no  rsc4\_Notify(Cmd;clients)  k  between  e'  and  e)))
                              \mwedge{}  (<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'))))))))


By

---

ProveILF\_instance  "vote""rsc4"



Home Index