Step
*
1
2
1
1
1
1
2
1
1
of Lemma
rsc4-agreement-property
.....assertion.....
1. Cmd : {T:Type| valueall-type(T)}
2. cmdeq : EqDecider(Cmd)
3. locs : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs : 
7. es : EO'
8. StandardAssumptions(rsc4_Main) es
9. bag-no-repeats(Id;locs)
10. bag-size(locs) = ((coeff * flrs) + flrs + 1)
11. e1 : E
12. e2 : E
13. c1 : Cmd
14. n : 
15. <n, c1> 
rsc4_decided'base(Cmd)(e1)
16. x1 : Id
17. r1 :
18. L1 : Id List
19. no_repeats(Id;L1)
20. ||L1|| = ((coeff * flrs) + 1)
21. (
vtrL1.(
e':E. <x1, make-Msg(``rsc4 vote``; 
Cmd Id;<<<n, r1>, c1>, vtr>)> rsc4_Main(e'))
vtr locs)
22. x : Id
23. 0 
(coeff * flrs)
24. e' : E
25. x2 : Id
26. y : Id
27. c : Cmd
28. loc(e') locs
29. x2 locs
30. y = loc(e')
31. e3 : {e1:E| e1 loc e' }
32. a2 :
33. b2 : List
34. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e3)
35. (a2 < n) 
(n b2)
36. b : Cmd
37. e4 : {e1:E| e1 loc e' }
38. b4 :
39. b4 Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e4)
40. True
41. e' = e4
42. (no rsc4_Notify(Cmd;clients) n between e3 and e')
43. True
44. <n, b> Base([propose]; Cmd)(e3)
(b1:. b3:Id. <<<n, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e3))
45. x3 : Id
46. cs : Cmd List
47. L : Id List
48. no_repeats(Id;L)
49. ||L|| = ((coeff * flrs) + 1)
50. ||cs|| = ||L||
51. i:||L||
((e':E. <x3, make-Msg(``rsc4 vote``; Cmd Id;<<<n, r1>, cs[i]>, L[i]>)> rsc4_Main(e')) L[i] locs)
52. c = (snd(poss-maj(cmdeq;cs;hd(cs))))
(((coeff - 1) * flrs) + 1) ||filter(
x.deq-member(IdDeq;x;L1);L)||
BY
{ (InstLemma `filter-split-length` [
Id
;
x.deq-member(IdDeq;x;L1);L]
THENA Auto) }
1
1. Cmd : {T:Type| valueall-type(T)}
2. cmdeq : EqDecider(Cmd)
3. locs : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs :
7. es : EO'
8. StandardAssumptions(rsc4_Main) es
9. bag-no-repeats(Id;locs)
10. bag-size(locs) = ((coeff * flrs) + flrs + 1)
11. e1 : E
12. e2 : E
13. c1 : Cmd
14. n :
15. <n, c1> rsc4_decided'base(Cmd)(e1)
16. x1 : Id
17. r1 :
18. L1 : Id List
19. no_repeats(Id;L1)
20. ||L1|| = ((coeff * flrs) + 1)
21. (vtrL1.(e':E. <x1, make-Msg(``rsc4 vote``; Cmd Id;<<<n, r1>, c1>, vtr>)> rsc4_Main(e'))
vtr locs)
22. x : Id
23. 0 (coeff * flrs)
24. e' : E
25. x2 : Id
26. y : Id
27. c : Cmd
28. loc(e') locs
29. x2 locs
30. y = loc(e')
31. e3 : {e1:E| e1 loc e' }
32. a2 :
33. b2 : List
34. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e3)
35. (a2 < n) (n b2)
36. b : Cmd
37. e4 : {e1:E| e1 loc e' }
38. b4 :
39. b4 Memory-class(rsc4_update_round(Cmd) n;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e4)
40. True
41. e' = e4
42. (no rsc4_Notify(Cmd;clients) n between e3 and e')
43. True
44. <n, b> Base([propose]; Cmd)(e3)
(b1:. b3:Id. <<<n, b1>, b>, b3> Base(``rsc4 vote``; Cmd Id)(e3))
45. x3 : Id
46. cs : Cmd List
47. L : Id List
48. no_repeats(Id;L)
49. ||L|| = ((coeff * flrs) + 1)
50. ||cs|| = ||L||
51. i:||L||
((e':E. <x3, make-Msg(``rsc4 vote``; Cmd Id;<<<n, r1>, cs[i]>, L[i]>)> rsc4_Main(e')) L[i] locs)
52. c = (snd(poss-maj(cmdeq;cs;hd(cs))))
53. (||filter(x.deq-member(IdDeq;x;L1);L)|| + ||filter(x.(
deq-member(IdDeq;x;L1));L)||) = ||L||
(((coeff - 1) * flrs) + 1) ||filter(x.deq-member(IdDeq;x;L1);L)||
.....assertion.....
1. Cmd : \{T:Type| valueall-type(T)\}
2. cmdeq : EqDecider(Cmd)
3. locs : bag(Id)
4. clients : bag(Id)
5. coeff : \{2...\}
6. flrs : \mBbbN{}
7. es : EO'
8. StandardAssumptions(rsc4\_Main) es
9. bag-no-repeats(Id;locs)
10. bag-size(locs) = ((coeff * flrs) + flrs + 1)
11. e1 : E
12. e2 : E
13. c1 : Cmd
14. n : \mBbbZ{}
15. <n, c1> \mmember{} rsc4\_decided'base(Cmd)(e1)
16. x1 : Id
17. r1 : \mBbbN{}
18. L1 : Id List
19. no\_repeats(Id;L1)
20. ||L1|| = ((coeff * flrs) + 1)
21. (\mforall{}vtr\mmember{}L1.(\mdownarrow{}\mexists{}e':E
<x1, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, r1>, c1>, vtr>)> \mmember{} rsc4\_Main(e'))
\mwedge{} vtr \mdownarrow{}\mmember{} locs)
22. x : Id
23. 0 \mleq{} (coeff * flrs)
24. e' : E
25. x2 : Id
26. y : Id
27. c : Cmd
28. loc(e') \mdownarrow{}\mmember{} locs
29. x2 \mdownarrow{}\mmember{} locs
30. y = loc(e')
31. e3 : \{e1:E| e1 \mleq{}loc e' \}
32. a2 : \mBbbZ{}
33. b2 : \mBbbZ{} List
34. <a2, b2> \mmember{} Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init() ɘ, []>rsc4\_Proposal(Cmd))(e3)
35. (a2 < n) \mvee{} (n \mmember{} b2)
36. b : Cmd
37. e4 : \{e1:E| e1 \mleq{}loc e' \}
38. b4 : \mBbbZ{}
39. b4 \mmember{} Memory-class(rsc4\_update\_round(Cmd) n;rsc4\_init() 0;rsc4\_RoundInfo(Cmd))(e4)
40. True
41. e' = e4
42. (no rsc4\_Notify(Cmd;clients) n between e3 and e')
43. True
44. <n, b> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e3)
\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<n, b1>, b>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e3))
45. x3 : Id
46. cs : Cmd List
47. L : Id List
48. no\_repeats(Id;L)
49. ||L|| = ((coeff * flrs) + 1)
50. ||cs|| = ||L||
51. \mforall{}i:\mBbbN{}||L||
((\mdownarrow{}\mexists{}e':E
<x3, make-Msg(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id;<<<n, r1>, cs[i]>, L[i]>)> \mmember{} rsc4\_Main(e'))
\mwedge{} L[i] \mdownarrow{}\mmember{} locs)
52. c = (snd(poss-maj(cmdeq;cs;hd(cs))))
\mvdash{} (((coeff - 1) * flrs) + 1) \mleq{} ||filter(\mlambda{}x.deq-member(IdDeq;x;L1);L)||
By
(InstLemma `filter-split-length` [\mkleeneopen{}Id\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.deq-member(IdDeq;x;L1)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{} THENA Auto)
Home
Index