---

Step * of Lemma rsc4-votes-consistent

[Cmd:ValueAllType]. [cmdeq:EqDecider(Cmd)]. [locs,clients:bag(Id)]. [coeff,flrs:]. [es:EO'].
  ((StandardAssumptions(rsc4_Main) es)
   (e1,e2:E. n,i:. x,y,z:Id. c1,c2:Cmd.
        (<y, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, i>, c1>, x>)>  rsc4_Main(e1)
         <z, make-Msg(``rsc4 vote``;    Cmd  Id;<<<n, i>, c2>, x>)>  rsc4_Main(e2)
         (c1 = c2))))
BY
{ (Unfold `vatype` 0
   THEN (UnivCD THENA MaAuto)
   THEN (RWO "rsc4-vote" (-2) THENA Auto)
   THEN (RWO "rsc4-vote" (-1) THENA Auto)
   THEN SquashExRepD
   THEN All DSet
   THEN All (\h. Try (Fold `rsc4_ReplicaState` h))) }

1
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>  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))
 ((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>  Base(``rsc4 vote``;    Cmd  Id)(e1))))
       (e2 = e1)))
   (no rsc4_Notify(Cmd;clients) n between e' and e2))
43. True
44. <n, b>  Base([propose];  Cmd)(e')
 (b1:. b3:Id. <<<n, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e'))
 c1 = c2

---

\mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[locs,clients:bag(Id)].  \mforall{}[coeff,flrs:\mBbbZ{}].  \mforall{}[es:EO'].
    ((StandardAssumptions(rsc4\_Main)  es)
    {}\mRightarrow{}  (\mforall{}e1,e2:E.  \mforall{}n,i:\mBbbZ{}.  \mforall{}x,y,z:Id.  \mforall{}c1,c2:Cmd.
                (<y,  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<n,  i>,  c1>,  x>)>  \mmember{}  rsc4\_Main(e1)
                {}\mRightarrow{}  <z,  make-Msg(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id;<<<n,  i>,  c2>,  x>)>  \mmember{}  rsc4\_Main(e2)
                {}\mRightarrow{}  (c1  =  c2))))


By

---

(Unfold  `vatype`  0
  THEN  (UnivCD  THENA  MaAuto)
  THEN  (RWO  "rsc4-vote"  (-2)  THENA  Auto)
  THEN  (RWO  "rsc4-vote"  (-1)  THENA  Auto)
  THEN  SquashExRepD
  THEN  All  DSet\mcdot{}
  THEN  All  (\mbackslash{}h.  Try  (Fold  `rsc4\_ReplicaState`  h)))



Home Index