---

Step * 1 1 1 of Lemma rsc4-votes-consistent


1. Cmd : Type
2. valueall-type(Cmd)
3. cmdeq : EqDecider(Cmd)
4. locs : bag(Id)
5. clients : bag(Id)
6. coeff : 
7. flrs : 
8. es : EO'
9. StandardAssumptions(rsc4_Main) es
10. e1 : E
11. e2 : E
12. n : 
13. i : 
14. x : Id
15. y : Id
16. z : Id
17. c1 : Cmd
18. c2 : Cmd
19. loc(e1)  locs
20. y  locs
21. x = loc(e1)
22. e3 : E
23. e3 loc e1 
24. a3 : 
25. b4 :  List
26. <a3, b4>  rsc4_ReplicaState(Cmd)(e3)
27. (a3 < n)  (n  b4)
28. b3 : Cmd
29. ((e1 = e3)  (c1 = b3)  (i = 0))
 ((e2:{e2:E| e2 loc e1 } 
      (((b4:. (b4  Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)  (b4 < i)))
       (<<n, i>, c1>  Base(``rsc4 retry``;    Cmd)(e2)  (b5:Id. <<<n, i>, c1>, b5>  rsc4_vote'base(Cmd)(e2))))
       (e1 = e2)))
   (no rsc4_Notify(Cmd;clients) n between e3 and e1))
30. True
31. <n, b3>  rsc4_propose'base(Cmd)(e3)  (b1:. b3@0:Id. <<<n, b1>, b3>, b3@0>  rsc4_vote'base(Cmd)(e3))
32. loc(e2)  locs
33. z  locs
34. x = loc(e2)
35. e' : E
36. e' loc e2 
37. a2 : 
38. b2 :  List
39. <a2, b2>  rsc4_ReplicaState(Cmd)(e')
40. (a2 < n)  (n  b2)
41. b : Cmd
42. ((e2 = e')  (c2 = b)  (i = 0))
 ((e1:{e1:E| e1 loc e2 } 
      (((b4:. (b4  Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e1)  (b4 < i)))
       (<<n, i>, c2>  Base(``rsc4 retry``;    Cmd)(e1)  (b5:Id. <<<n, i>, c2>, b5>  rsc4_vote'base(Cmd)(e1))))
       (e2 = e1)))
   (no rsc4_Notify(Cmd;clients) n between e' and e2))
43. True
44. <n, b>  rsc4_propose'base(Cmd)(e')  (b1:. b3:Id. <<<n, b1>, b>, b3>  rsc4_vote'base(Cmd)(e'))
 <n, b3>  rsc4_propose'base(Cmd)(e3)  <n, b3>  rsc4_vote2prop(Cmd)@|Loc, rsc4_vote'base(Cmd)|(e3)
BY
{ (ParallelOp -14
   THEN MaAuto
   THEN ExRepD
   THEN MaUseClassRel'' 0
   THEN D 0
   THEN InstConcl [<<<n, b1>, b3>, b3@0>]
   THEN MaAuto
   THEN RepUR ``rsc4_vote2prop`` 0
   THEN BagMemberD 0
   THEN Auto) }

---

1.  Cmd  :  Type
2.  valueall-type(Cmd)
3.  cmdeq  :  EqDecider(Cmd)
4.  locs  :  bag(Id)
5.  clients  :  bag(Id)
6.  coeff  :  \mBbbZ{}
7.  flrs  :  \mBbbZ{}
8.  es  :  EO'
9.  StandardAssumptions(rsc4\_Main)  es
10.  e1  :  E
11.  e2  :  E
12.  n  :  \mBbbZ{}
13.  i  :  \mBbbZ{}
14.  x  :  Id
15.  y  :  Id
16.  z  :  Id
17.  c1  :  Cmd
18.  c2  :  Cmd
19.  loc(e1)  \mdownarrow{}\mmember{}  locs
20.  y  \mdownarrow{}\mmember{}  locs
21.  x  =  loc(e1)
22.  e3  :  E
23.  e3  \mleq{}loc  e1 
24.  a3  :  \mBbbZ{}
25.  b4  :  \mBbbZ{}  List
26.  <a3,  b4>  \mmember{}  rsc4\_ReplicaState(Cmd)(e3)
27.  (a3  <  n)  \mvee{}  (n  \mmember{}  b4)
28.  b3  :  Cmd
29.  ((e1  =  e3)  \mwedge{}  (c1  =  b3)  \mwedge{}  (i  =  0))
\mvee{}  ((\mdownarrow{}\mexists{}e2:\{e2:E|  e2  \mleq{}loc  e1  \} 
            (((\mdownarrow{}\mexists{}b4:\mBbbZ{}
                      (b4  \mmember{}  Memory-class(rsc4\_update\_round(Cmd)  n;rsc4\_init()  0;rsc4\_RoundInfo(Cmd))(e2)
                      \mwedge{}  (b4  <  i)))
            \mwedge{}  (<<n,  i>,  c1>  \mmember{}  Base(``rsc4  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)(e2)
                \mdownarrow{}\mvee{}  (\mexists{}b5:Id.  <<<n,  i>,  c1>,  b5>  \mmember{}  rsc4\_vote'base(Cmd)(e2))))
            \mwedge{}  (e1  =  e2)))
    \mwedge{}  (no  rsc4\_Notify(Cmd;clients)  n  between  e3  and  e1))
30.  True
31.  <n,  b3>  \mmember{}  rsc4\_propose'base(Cmd)(e3)
\mvee{}  (\mexists{}b1:\mBbbZ{}.  \mexists{}b3@0:Id.  <<<n,  b1>,  b3>,  b3@0>  \mmember{}  rsc4\_vote'base(Cmd)(e3))
32.  loc(e2)  \mdownarrow{}\mmember{}  locs
33.  z  \mdownarrow{}\mmember{}  locs
34.  x  =  loc(e2)
35.  e'  :  E
36.  e'  \mleq{}loc  e2 
37.  a2  :  \mBbbZ{}
38.  b2  :  \mBbbZ{}  List
39.  <a2,  b2>  \mmember{}  rsc4\_ReplicaState(Cmd)(e')
40.  (a2  <  n)  \mvee{}  (n  \mmember{}  b2)
41.  b  :  Cmd
42.  ((e2  =  e')  \mwedge{}  (c2  =  b)  \mwedge{}  (i  =  0))
\mvee{}  ((\mdownarrow{}\mexists{}e1:\{e1:E|  e1  \mleq{}loc  e2  \} 
            (((\mdownarrow{}\mexists{}b4:\mBbbZ{}
                      (b4  \mmember{}  Memory-class(rsc4\_update\_round(Cmd)  n;rsc4\_init()  0;rsc4\_RoundInfo(Cmd))(e1)
                      \mwedge{}  (b4  <  i)))
            \mwedge{}  (<<n,  i>,  c2>  \mmember{}  Base(``rsc4  retry``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)(e1)
                \mdownarrow{}\mvee{}  (\mexists{}b5:Id.  <<<n,  i>,  c2>,  b5>  \mmember{}  rsc4\_vote'base(Cmd)(e1))))
            \mwedge{}  (e2  =  e1)))
    \mwedge{}  (no  rsc4\_Notify(Cmd;clients)  n  between  e'  and  e2))
43.  True
44.  <n,  b>  \mmember{}  rsc4\_propose'base(Cmd)(e')
\mvee{}  (\mexists{}b1:\mBbbZ{}.  \mexists{}b3:Id.  <<<n,  b1>,  b>,  b3>  \mmember{}  rsc4\_vote'base(Cmd)(e'))
\mvdash{}  <n,  b3>  \mmember{}  rsc4\_propose'base(Cmd)(e3)
\mvee{}  <n,  b3>  \mmember{}  rsc4\_vote2prop(Cmd)@|Loc,  rsc4\_vote'base(Cmd)|(e3)


By

---

(ParallelOp  -14
  THEN  MaAuto
  THEN  ExRepD
  THEN  MaUseClassRel''  0
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}<<<n,  b1>,  b3>,  b3@0>\mkleeneclose{}]\mcdot{}
  THEN  MaAuto
  THEN  RepUR  ``rsc4\_vote2prop``  0
  THEN  BagMemberD  0
  THEN  Auto)



Home Index