---

Step * 1 2 3 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. (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>  Base(``rsc4 vote``;    Cmd  Id)(e2))))
        (e1 = e2)))
 (no rsc4_Notify(Cmd;clients) n between e3 and e1)
30. True
31. <n, b3>  Base([propose];  Cmd)(e3)
 (b1:. b3@0:Id. <<<n, b1>, b3>, b3@0>  Base(``rsc4 vote``;    Cmd  Id)(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)
43. True
44. <n, b>  Base([propose];  Cmd)(e')
 (b1:. b3:Id. <<<n, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e'))
45. e' = e3
 c1 = c2
BY
{ (SquashExRepD
   THEN Assert 0  b5
   THEN Auto'
   THEN (Assert b5  rsc4_NewRoundsState(Cmd) n(e4) THENA (RepUR ``rsc4_NewRoundsState`` 0 THEN Trivial))
   THEN FLemma `rsc4_pos_rounds` [-1]
   THEN MaAuto
   THEN RW assert_pushdownC (-1)
   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.  (\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{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e2))))
              \mwedge{}  (e1  =  e2)))
\mwedge{}  (no  rsc4\_Notify(Cmd;clients)  n  between  e3  and  e1)
30.  True
31.  <n,  b3>  \mmember{}  Base([propose];\mBbbZ{}  \mtimes{}  Cmd)(e3)
\mvee{}  (\mexists{}b1:\mBbbZ{}.  \mexists{}b3@0:Id.  <<<n,  b1>,  b3>,  b3@0>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(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)
43.  True
44.  <n,  b>  \mmember{}  Base([propose];\mBbbZ{}  \mtimes{}  Cmd)(e')
\mvee{}  (\mexists{}b1:\mBbbZ{}.  \mexists{}b3:Id.  <<<n,  b1>,  b>,  b3>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e'))
45.  e'  =  e3
\mvdash{}  c1  =  c2


By

---

(SquashExRepD
  THEN  Assert  \mkleeneopen{}0  \mleq{}  b5\mkleeneclose{}\mcdot{}
  THEN  Auto'
  THEN  (Assert  \mkleeneopen{}b5  \mmember{}  rsc4\_NewRoundsState(Cmd)  n(e4)\mkleeneclose{}\mcdot{}
              THENA  (RepUR  ``rsc4\_NewRoundsState``  0  THEN  Trivial)
              )
  THEN  FLemma  `rsc4\_pos\_rounds`  [-1]
  THEN  MaAuto
  THEN  RW  assert\_pushdownC  (-1)
  THEN  Auto)



Home Index