Step
*
3
2
1
2
of Lemma
rsc4-validity-property
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. e : E
10. 
e1:E
((e1 < e)
((v:
Cmd. (v 
rsc4_decided'base(Cmd)(e1) (
e':E. ((e' < e1) 
v rsc4_propose'base(Cmd)(e')))))
(v: Cmd Id
(v rsc4_vote'base(Cmd)(e1)
(e':E. ((e' < e1) <fst(fst(fst(v))), snd(fst(v))> rsc4_propose'base(Cmd)(e')))))
(v: Cmd
(v rsc4_retry'base(Cmd)(e1)
(e':E. ((e' < e1) <fst(fst(v)), snd(v)> rsc4_propose'base(Cmd)(e')))))
(e2:E
(e2 c
e1
(cs:Cmd List. L:Id List. n,rnd:. c:Cmd.
(<cs, L> rsc4_QuorumState(Cmd) <n, rnd>(e1)
(c cs)
(e':E. ((e' < e1) <n, c> rsc4_propose'base(Cmd)(e')))))))))
11. n1 :
12. n :
13. c3 : Cmd
14. <<n1, n>, c3> rsc4_retry'base(Cmd)(e)
15. e' : E
16. (e' < e)
17. loc(e') locs
18. loc(e) = loc(e')
19. e1 : {e1:E| e1 loc e' }
20. a :
21. a2 :
22. b2 : List
23. <a2, b2> Memory-class(rsc4_update_replica(Cmd);rsc4_init() <0, []>;rsc4_Proposal(Cmd))(e1)
24. (a2 < a) 
(a b2)
25. c2 : Cmd
26. True
27. <a, c2> Base([propose]; Cmd)(e1)
(b1:. b3:Id. <<<a, b1>, c2>, b3> Base(``rsc4 vote``; Cmd Id)(e1))
28. e2 : {e1:E| e1 loc e' }
29. b3 :
30. b6 :
31. b6 Memory-class(rsc4_update_round(Cmd) a;rsc4_init() 0;rsc4_RoundInfo(Cmd))(e2)
32. b6 < b3
33. c1 : Cmd
34. True
35. <<a, b3>, c1> Base(``rsc4 retry``; Cmd)(e2)
(b5@0:Id. <<<a, b3>, c1>, b5@0> Base(``rsc4 vote``; Cmd Id)(e2))
36. b1 :
37. n = (b1 + 1)
38. cmd : Cmd
39. loc : Id
40. <<<n1, b1>, cmd>, loc> Base(``rsc4 vote``; Cmd Id)(e')
41. cs : Cmd List
42. ||cs|| = (coeff * flrs)
43. 
((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
44. c3 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
45. L : Id List
46. <cs, L> rsc4_QuorumState(Cmd) <a, b3>(e')
47. a = n1
48. b3 = b1
49. (loc L)
50. (no rsc4_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
51. (no rsc4_Notify(Cmd;clients) a between e1 and e')
52. (c3 cs)
53. v: Cmd. (v rsc4_decided'base(Cmd)(e') (e'@0:E. ((e'@0 < e') v rsc4_propose'base(Cmd)(e'@0))))
54. v: Cmd Id
(v rsc4_vote'base(Cmd)(e')
(e'@0:E. ((e'@0 < e') <fst(fst(fst(v))), snd(fst(v))> rsc4_propose'base(Cmd)(e'@0))))
55. v: Cmd
(v rsc4_retry'base(Cmd)(e') (e'@0:E. ((e'@0 < e') <fst(fst(v)), snd(v)> rsc4_propose'base(Cmd)(e'@0))))
56. e2:E
(e2 c e'
(cs:Cmd List. L:Id List. n,rnd:. c:Cmd.
(<cs, L> rsc4_QuorumState(Cmd) <n, rnd>(e')
(c cs)
(e'@0:E. ((e'@0 < e') <n, c> rsc4_propose'base(Cmd)(e'@0))))))
e':E. ((e' < e) <n1, c3> rsc4_propose'base(Cmd)(e'))
BY
{ Try (((InstHyp [
e2
;cs;L;a;b3;c3] (-1)
THENA MaAuto) THEN RepeatFor 3 (ParallelLast) THEN MaAuto)) }
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. e : E
10. \mforall{}e1:E
((e1 < e)
{}\mRightarrow{} ((\mforall{}v:\mBbbZ{} \mtimes{} Cmd
(v \mmember{} rsc4\_decided'base(Cmd)(e1)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} v \mmember{} rsc4\_propose'base(Cmd)(e')))))
\mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id
(v \mmember{} rsc4\_vote'base(Cmd)(e1)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E
((e' < e1) \mwedge{} <fst(fst(fst(v))), snd(fst(v))> \mmember{} rsc4\_propose'base(Cmd)(e')))))
\mwedge{} (\mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd
(v \mmember{} rsc4\_retry'base(Cmd)(e1)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} <fst(fst(v)), snd(v)> \mmember{} rsc4\_propose'base(Cmd)(e')))))
\mwedge{} (\mforall{}e2:E
(e2 c\mleq{} e1
{}\mRightarrow{} (\mforall{}cs:Cmd List. \mforall{}L:Id List. \mforall{}n,rnd:\mBbbZ{}. \mforall{}c:Cmd.
(<cs, L> \mmember{} rsc4\_QuorumState(Cmd) <n, rnd>(e1)
{}\mRightarrow{} (c \mmember{} cs)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e':E. ((e' < e1) \mwedge{} <n, c> \mmember{} rsc4\_propose'base(Cmd)(e')))))))))
11. n1 : \mBbbZ{}
12. n : \mBbbZ{}
13. c3 : Cmd
14. <<n1, n>, c3> \mmember{} rsc4\_retry'base(Cmd)(e)
15. e' : E
16. (e' < e)
17. loc(e') \mdownarrow{}\mmember{} locs
18. loc(e) = loc(e')
19. e1 : \{e1:E| e1 \mleq{}loc e' \}
20. a : \mBbbZ{}
21. a2 : \mBbbZ{}
22. b2 : \mBbbZ{} List
23. <a2, b2> \mmember{} Memory-class(rsc4\_update\_replica(Cmd);rsc4\_init() ɘ, []>rsc4\_Proposal(Cmd))(e1)
24. (a2 < a) \mvee{} (a \mmember{} b2)
25. c2 : Cmd
26. True
27. <a, c2> \mmember{} Base([propose];\mBbbZ{} \mtimes{} Cmd)(e1)
\mvee{} (\mexists{}b1:\mBbbZ{}. \mexists{}b3:Id. <<<a, b1>, c2>, b3> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e1))
28. e2 : \{e1:E| e1 \mleq{}loc e' \}
29. b3 : \mBbbZ{}
30. b6 : \mBbbZ{}
31. b6 \mmember{} Memory-class(rsc4\_update\_round(Cmd) a;rsc4\_init() 0;rsc4\_RoundInfo(Cmd))(e2)
32. b6 < b3
33. c1 : Cmd
34. True
35. <<a, b3>, c1> \mmember{} Base(``rsc4 retry``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)(e2)
\mvee{} (\mexists{}b5@0:Id. <<<a, b3>, c1>, b5@0> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e2))
36. b1 : \mBbbZ{}
37. n = (b1 + 1)
38. cmd : Cmd
39. loc : Id
40. <<<n1, b1>, cmd>, loc> \mmember{} Base(``rsc4 vote``;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)(e')
41. cs : Cmd List
42. ||cs|| = (coeff * flrs)
43. \mneg{}((fst(poss-maj(cmdeq;[cmd / cs];cmd))) = ((coeff * flrs) + 1))
44. c3 = (snd(poss-maj(cmdeq;[cmd / cs];cmd)))
45. L : Id List
46. <cs, L> \mmember{} rsc4\_QuorumState(Cmd) <a, b3>(e')
47. a = n1
48. b3 = b1
49. \mneg{}(loc \mmember{} L)
50. (no rsc4\_Quorum(Cmd;cmdeq;coeff;flrs) <a, b3> between e2 and e')
51. (no rsc4\_Notify(Cmd;clients) a between e1 and e')
52. (c3 \mmember{} cs)
53. \mforall{}v:\mBbbZ{} \mtimes{} Cmd
(v \mmember{} rsc4\_decided'base(Cmd)(e')
{}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E. ((e'@0 < e') \mwedge{} v \mmember{} rsc4\_propose'base(Cmd)(e'@0))))
54. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id
(v \mmember{} rsc4\_vote'base(Cmd)(e')
{}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E. ((e'@0 < e') \mwedge{} <fst(fst(fst(v))), snd(fst(v))> \mmember{} rsc4\_propose'base(Cmd)(e'@0))))
55. \mforall{}v:\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd
(v \mmember{} rsc4\_retry'base(Cmd)(e')
{}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E. ((e'@0 < e') \mwedge{} <fst(fst(v)), snd(v)> \mmember{} rsc4\_propose'base(Cmd)(e'@0))))
56. \mforall{}e2:E
(e2 c\mleq{} e'
{}\mRightarrow{} (\mforall{}cs:Cmd List. \mforall{}L:Id List. \mforall{}n,rnd:\mBbbZ{}. \mforall{}c:Cmd.
(<cs, L> \mmember{} rsc4\_QuorumState(Cmd) <n, rnd>(e')
{}\mRightarrow{} (c \mmember{} cs)
{}\mRightarrow{} (\mdownarrow{}\mexists{}e'@0:E. ((e'@0 < e') \mwedge{} <n, c> \mmember{} rsc4\_propose'base(Cmd)(e'@0))))))
\mvdash{} \mdownarrow{}\mexists{}e':E. ((e' < e) \mwedge{} <n1, c3> \mmember{} rsc4\_propose'base(Cmd)(e'))
By
Try (((InstHyp [\mkleeneopen{}e2\mkleeneclose{};\mkleeneopen{}cs\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b3\mkleeneclose{};\mkleeneopen{}c3\mkleeneclose{}] (-1)\mcdot{} THENA MaAuto)
THEN RepeatFor 3 (ParallelLast)
THEN MaAuto))\mcdot{}
Home
Index