---

Step * 1 2 1 4 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. b4 :  List
25. b3 : Cmd
26. (e1 = e3)  (c1 = b3)  (i = 0)
27. True
28. b1:. b3@0:Id. <<<n, b1>, b3>, b3@0>  Base(``rsc4 vote``;    Cmd  Id)(e3)
29. loc(e2)  locs
30. z  locs
31. x = loc(e2)
32. e' : E
33. e' loc e2 
34. b2 :  List
35. b : Cmd
36. (e2 = e')  (c2 = b)  (i = 0)
37. True
38. b1:. b3:Id. <<<n, b1>, b>, b3>  Base(``rsc4 vote``;    Cmd  Id)(e')
39. e' = e3
 c1 = c2
BY
{ ExRepD }

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. b4 :  List
25. b3 : Cmd
26. e1 = e3
27. c1 = b3
28. i = 0
29. True
30. b6 : 
31. b3@0 : Id
32. <<<n, b6>, b3>, b3@0>  Base(``rsc4 vote``;    Cmd  Id)(e3)
33. loc(e2)  locs
34. z  locs
35. x = loc(e2)
36. e' : E
37. e' loc e2 
38. b2 :  List
39. b : Cmd
40. e2 = e'
41. c2 = b
42. i = 0
43. True
44. b1 : 
45. b5 : Id
46. <<<n, b1>, b>, b5>  Base(``rsc4 vote``;    Cmd  Id)(e')
47. e' = e3
 c1 = c2

---

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.  b4  :  \mBbbZ{}  List
25.  b3  :  Cmd
26.  (e1  =  e3)  \mwedge{}  (c1  =  b3)  \mwedge{}  (i  =  0)
27.  True
28.  \mexists{}b1:\mBbbZ{}.  \mexists{}b3@0:Id.  <<<n,  b1>,  b3>,  b3@0>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e3)
29.  loc(e2)  \mdownarrow{}\mmember{}  locs
30.  z  \mdownarrow{}\mmember{}  locs
31.  x  =  loc(e2)
32.  e'  :  E
33.  e'  \mleq{}loc  e2 
34.  b2  :  \mBbbZ{}  List
35.  b  :  Cmd
36.  (e2  =  e')  \mwedge{}  (c2  =  b)  \mwedge{}  (i  =  0)
37.  True
38.  \mexists{}b1:\mBbbZ{}.  \mexists{}b3:Id.  <<<n,  b1>,  b>,  b3>  \mmember{}  Base(``rsc4  vote``;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)(e')
39.  e'  =  e3
\mvdash{}  c1  =  c2


By

---

ExRepD



Home Index