Proof of Nuprl Lemma : rsc4-votes-consistent

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

.....assertion.....
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. e5 : {e2:E| e2

loc e1 }
30. b6 :

31. b6

Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e5)
32. b6 < i
33. True
34. <<n, i>, c1>

Base(``rsc4 retry``;

Cmd)(e5)

(

b5:Id. <<<n, i>, c1>, b5>

Base(``rsc4 vote``;

Cmd

Id)(e5))
35. e1 = e5
36. (no rsc4_Notify(Cmd;clients) n between e3 and e1)
37. True
38. <n, b3>

Base([propose];

Cmd)(e3)

(

b1:

.

b3@0:Id. <<<n, b1>, b3>, b3@0>

Base(``rsc4 vote``;

Cmd

Id)(e3))
39. loc(e2)

locs
40. z

locs
41. x = loc(e2)
42. e' : E
43. e'

loc e2
44. a2 :

45. b2 :

List
46. <a2, b2>

rsc4_ReplicaState(Cmd)(e')
47. (a2 < n)

(n

b2)
48. b : Cmd
49. e4 : {e1:E| e1

loc e2 }
50. b5 :

51. b5

Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e4)
52. b5 < i
53. True
54. <<n, i>, c2>

Base(``rsc4 retry``;

Cmd)(e4)

(

b5:Id. <<<n, i>, c2>, b5>

Base(``rsc4 vote``;

Cmd

Id)(e4))
55. e2 = e4
56. (no rsc4_Notify(Cmd;clients) n between e' and e2)
57. True
58. <n, b>

Base([propose];

Cmd)(e')

(

b1:

.

b3:Id. <<<n, b1>, b>, b3>

Base(``rsc4 vote``;

Cmd

Id)(e'))
59. e' = e3

e2 = e1
BY
{ (UseEsLoclTri

es

e1

e2

THEN D (-1)) }

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. e5 : {e2:E| e2

loc e1 }
30. b6 :

31. b6

Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e5)
32. b6 < i
33. True
34. <<n, i>, c1>

Base(``rsc4 retry``;

Cmd)(e5)

(

b5:Id. <<<n, i>, c1>, b5>

Base(``rsc4 vote``;

Cmd

Id)(e5))
35. e1 = e5
36. (no rsc4_Notify(Cmd;clients) n between e3 and e1)
37. True
38. <n, b3>

Base([propose];

Cmd)(e3)

(

b1:

.

b3@0:Id. <<<n, b1>, b3>, b3@0>

Base(``rsc4 vote``;

Cmd

Id)(e3))
39. loc(e2)

locs
40. z

locs
41. x = loc(e2)
42. e' : E
43. e'

loc e2
44. a2 :

45. b2 :

List
46. <a2, b2>

rsc4_ReplicaState(Cmd)(e')
47. (a2 < n)

(n

b2)
48. b : Cmd
49. e4 : {e1:E| e1

loc e2 }
50. b5 :

51. b5

Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e4)
52. b5 < i
53. True
54. <<n, i>, c2>

Base(``rsc4 retry``;

Cmd)(e4)

(

b5:Id. <<<n, i>, c2>, b5>

Base(``rsc4 vote``;

Cmd

Id)(e4))
55. e2 = e4
56. (no rsc4_Notify(Cmd;clients) n between e' and e2)
57. True
58. <n, b>

Base([propose];

Cmd)(e')

(

b1:

.

b3:Id. <<<n, b1>, b>, b3>

Base(``rsc4 vote``;

Cmd

Id)(e'))
59. e' = e3
60. (e1 <loc e2)

e2 = e1

2
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. e5 : {e2:E| e2

loc e1 }
30. b6 :

31. b6

Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e5)
32. b6 < i
33. True
34. <<n, i>, c1>

Base(``rsc4 retry``;

Cmd)(e5)

(

b5:Id. <<<n, i>, c1>, b5>

Base(``rsc4 vote``;

Cmd

Id)(e5))
35. e1 = e5
36. (no rsc4_Notify(Cmd;clients) n between e3 and e1)
37. True
38. <n, b3>

Base([propose];

Cmd)(e3)

(

b1:

.

b3@0:Id. <<<n, b1>, b3>, b3@0>

Base(``rsc4 vote``;

Cmd

Id)(e3))
39. loc(e2)

locs
40. z

locs
41. x = loc(e2)
42. e' : E
43. e'

loc e2
44. a2 :

45. b2 :

List
46. <a2, b2>

rsc4_ReplicaState(Cmd)(e')
47. (a2 < n)

(n

b2)
48. b : Cmd
49. e4 : {e1:E| e1

loc e2 }
50. b5 :

51. b5

Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e4)
52. b5 < i
53. True
54. <<n, i>, c2>

Base(``rsc4 retry``;

Cmd)(e4)

(

b5:Id. <<<n, i>, c2>, b5>

Base(``rsc4 vote``;

Cmd

Id)(e4))
55. e2 = e4
56. (no rsc4_Notify(Cmd;clients) n between e' and e2)
57. True
58. <n, b>

Base([propose];

Cmd)(e')

(

b1:

.

b3:Id. <<<n, b1>, b>, b3>

Base(``rsc4 vote``;

Cmd

Id)(e'))
59. e' = e3
60. (e1 = e2)

(e2 <loc e1)

e2 = e1

.....assertion..... 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. e5 : \{e2:E| e2 \mleq{}loc e1 \} 30. b6 : \mBbbZ{} 31. b6 \mmember{} Memory-class(rsc4\_update\_round(Cmd) n;rsc4\_init() 0;rsc4\_RoundInfo(Cmd))(e5) 32. b6 < i 33. True 34. <<n, i>, c1> \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e5) \mvee{} (\mexists{}b5:Id. <<<n, i>, c1>, b5> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e5)) 35. e1 = e5 36. (no rsc4\_Notify(Cmd;clients) n between e3 and e1) 37. True 38. <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)) 39. loc(e2) \mdownarrow{}\mmember{} locs 40. z \mdownarrow{}\mmember{} locs 41. x = loc(e2) 42. e' : E 43. e' \mleq{}loc e2 44. a2 : \mBbbZ{} 45. b2 : \mBbbZ{} List 46. <a2, b2> \mmember{} rsc4\_ReplicaState(Cmd)(e') 47. (a2 < n) \mvee{} (n \mmember{} b2) 48. b : Cmd 49. e4 : \{e1:E| e1 \mleq{}loc e2 \} 50. b5 : \mBbbZ{} 51. b5 \mmember{} Memory-class(rsc4\_update\_round(Cmd) n;rsc4\_init() 0;rsc4\_RoundInfo(Cmd))(e4) 52. b5 < i 53. True 54. <<n, i>, c2> \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e4) \mvee{} (\mexists{}b5:Id. <<<n, i>, c2>, b5> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e4)) 55. e2 = e4 56. (no rsc4\_Notify(Cmd;clients) n between e' and e2) 57. True 58. <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')) 59. e' = e3 \mvdash{} e2 = e1 By (UseEsLoclTri \mkleeneopen{}es\mkleeneclose{}\mkleeneopen{}e1\mkleeneclose{}\mkleeneopen{}e2\mkleeneclose{}\mcdot{} THEN D (-1)) Home Index