Step
*
1
2
2
1
1
1
of Lemma
new_23_sig_agreement
.....antecedent.....
1. Cmd : {T:Type| valueall-type(T)}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
13. bag-no-repeats(Id;reps)@i
14. #(reps) = ((coeff * flrs) + flrs + 1) ∈ ℤ@i
15. (f propose) = (ℤ × Cmd) ∈ Type
16. (f notify) = (ℤ × Cmd) ∈ Type
17. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
18. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
19. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
20. f ∈ Name ─→ Type
21. e1 : E@i
22. e2 : E@i
23. n : ℤ@i
24. c1 : Cmd@i
25. <n, c1> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e2)@i
26. x : Id
27. x1 : Id
28. r1 : ℕ
29. L1 : Id List
30. no_repeats(Id;L1)
31. ||L1|| = ((coeff * flrs) + 1) ∈ ℤ
32. (∀vtr∈L1.↓∃e':E. mk-msg-interface(x1;make-Msg(``new_23_sig vote``;<<<n, r1>, c1>, vtr>)) ∈ new_23_sig_main()(e'))
33. 0 ≤ (coeff * flrs)
34. k : ℕ
35. ∀k:ℕk. ∀e':E. ∀x,y:Id. ∀c:Cmd. (mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, (r1 + 1) + k>, c>, y>)) ∈ new\000C_23_sig_main()(e') ⇒ (c = c1 ∈ Cmd))
36. e' : E@i
37. ∀e3:E. ((e3 < e') ⇒ (∀x,y:Id. ∀c:Cmd. (mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, (r1 + 1) + k>, c>, y>\000C)) ∈ new_23_sig_main()(e3) ⇒ (c = c1 ∈ Cmd))))
38. x2 : Id@i
39. y : Id@i
40. c : Cmd@i
41. loc(e') ↓∈ reps
42. e3 : {e1:E| e1 ≤loc e' }
43. z2 : Cmd
44. ((header(e3) = propose ∈ Name) ∧ has-es-info-type(es;e3;f;ℤ × Cmd) ∧ (<n, z2> = msgval(e3) ∈ (ℤ × Cmd)))
∨ ((header(e3) = ``new_23_sig vote`` ∈ Name)
∧ has-es-info-type(es;e3;f;ℤ × ℤ × Cmd × Id)
∧ (n = (fst(fst(fst(msgval(e3))))) ∈ ℤ)
∧ (z2 = (snd(fst(msgval(e3)))) ∈ Cmd))
45. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e3))
46. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e3 and e')
47. x2 ↓∈ reps
48. 0 = 0 ∈ ℤ
49. ff = ff
50. y = loc(e') ∈ Id
51. new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e') < (r1 + 1) + k
52. header(e') = ``new_23_sig retry`` ∈ Name
53. has-es-info-type(es;e';f;ℤ × ℤ × Cmd)
54. <<n, (r1 + 1) + k>, c> = msgval(e') ∈ (ℤ × ℤ × Cmd)
55. <<n, (r1 + k) + 1>, c> ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e')
56. x3 : Id
57. cs : Cmd List+
58. L : Id List
59. no_repeats(Id;L)
60. ||L|| = ((coeff * flrs) + 1) ∈ ℤ
61. ||cs|| = ||L|| ∈ ℤ
62. ∀i:ℕ||L||. ((↓∃e':E. mk-msg-interface(x3;make-Msg(``new_23_sig vote``;<<<n, r1 + k>, cs[i]>, L[i]>)) ∈ new_23_sig_ma\000Cin()(e')) ∧ L[i] ↓∈ reps)
63. c = (snd(poss-maj(eq;cs;hd(cs)))) ∈ Cmd
64. 0 < k
⊢ ||cs|| < 2 * count(eq c1;cs)
BY
{ (RWO "count-all" 0
THEN Auto'
THEN BLemma `l_all_iff`
THEN Auto
THEN RepeatFor 2 (D (-1))
THEN (InstHyp [⌈i⌉] (-7)⋅ THENA Auto')
THEN SquashExRepD
THEN OnMaybeHyp 35 (\h. ((InstHyp [⌈k - 1⌉] h⋅ THENA Auto')
THEN (Subst' (r1 + 1) + (k - 1) ~ r1 + k -1 THEN Auto)
THEN FHyp (-1) [-3]
THEN Complete (Auto)))) }
Latex:
Latex:
.....antecedent.....
1. Cmd : \{T:Type| valueall-type(T)\}
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : \{2...\}
6. flrs : \mBbbN{}
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig\{i:l\}(\mBbbZ{})
10. f : new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)
11. es : EO+(Message(f))
12. new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
13. bag-no-repeats(Id;reps)@i
14. \#(reps) = ((coeff * flrs) + flrs + 1)@i
15. (f propose) = (\mBbbZ{} \mtimes{} Cmd)
16. (f notify) = (\mBbbZ{} \mtimes{} Cmd)
17. (f ``new\_23\_sig decided``) = (\mBbbZ{} \mtimes{} Cmd)
18. (f ``new\_23\_sig retry``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
19. (f ``new\_23\_sig vote``) = (\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
20. f \mmember{} Name {}\mrightarrow{} Type
21. e1 : E@i
22. e2 : E@i
23. n : \mBbbZ{}@i
24. c1 : Cmd@i
25. <n, c1> \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e2)@i
26. x : Id
27. x1 : Id
28. r1 : \mBbbN{}
29. L1 : Id List
30. no\_repeats(Id;L1)
31. ||L1|| = ((coeff * flrs) + 1)
32. (\mforall{}vtr\mmember{}L1.\mdownarrow{}\mexists{}e':E. mk-msg-interface(x1;make-Msg(``new\_23\_sig vote``;<<<n, r1>, c1>, vtr>)) \mmember{} new\_2\000C3\_sig\_main()(e'))
33. 0 \mleq{} (coeff * flrs)
34. k : \mBbbN{}
35. \mforall{}k:\mBbbN{}k. \mforall{}e':E. \mforall{}x,y:Id. \mforall{}c:Cmd.
(mk-msg-interface(x;make-Msg(``new\_23\_sig vote``;<<<n, (r1 + 1) + k>, c>, y>)) \mmember{} new\_23\_sig\_ma\000Cin()(e') {}\mRightarrow{} (c = c1))
36. e' : E@i
37. \mforall{}e3:E
((e3 < e')
{}\mRightarrow{} (\mforall{}x,y:Id. \mforall{}c:Cmd.
(mk-msg-interface(x;make-Msg(``new\_23\_sig vote``;<<<n, (r1 + 1) + k>, c>, y>)) \mmember{} new\_23\_\000Csig\_main()(e3) {}\mRightarrow{} (c = c1))))
38. x2 : Id@i
39. y : Id@i
40. c : Cmd@i
41. loc(e') \mdownarrow{}\mmember{} reps
42. e3 : \{e1:E| e1 \mleq{}loc e' \}
43. z2 : Cmd
44. ((header(e3) = propose) \mwedge{} has-es-info-type(es;e3;f;\mBbbZ{} \mtimes{} Cmd) \mwedge{} (<n, z2> = msgval(e3)))
\mvee{} ((header(e3) = ``new\_23\_sig vote``)
\mwedge{} has-es-info-type(es;e3;f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd \mtimes{} Id)
\mwedge{} (n = (fst(fst(fst(msgval(e3))))))
\mwedge{} (z2 = (snd(fst(msgval(e3))))))
45. \mneg{}\muparrow{}(set-sig-member(slots) n new\_23\_sig\_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e3))
46. (no new\_23\_sig\_Notify(Cmd;clients;notify;propose;f) n between e3 and e')
47. x2 \mdownarrow{}\mmember{} reps
48. 0 = 0
49. ff = ff
50. y = loc(e')
51. new\_23\_sig\_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e') < (r1 + 1) + k
52. header(e') = ``new\_23\_sig retry``
53. has-es-info-type(es;e';f;\mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} Cmd)
54. <<n, (r1 + 1) + k>, c> = msgval(e')
55. <<n, (r1 + k) + 1>, c> \mmember{} new\_23\_sig\_retry'base(Cmd;notify;propose;f)(e')
56. x3 : Id
57. cs : Cmd List\msupplus{}
58. L : Id List
59. no\_repeats(Id;L)
60. ||L|| = ((coeff * flrs) + 1)
61. ||cs|| = ||L||
62. \mforall{}i:\mBbbN{}||L||
((\mdownarrow{}\mexists{}e':E. mk-msg-interface(x3;make-Msg(``new\_23\_sig vote``;<<<n, r1 + k>, cs[i]>, L[i]>)) \mmember{} ne\000Cw\_23\_sig\_main()(e')) \mwedge{} L[i] \mdownarrow{}\mmember{} reps)
63. c = (snd(poss-maj(eq;cs;hd(cs))))
64. 0 < k
\mvdash{} ||cs|| < 2 * count(eq c1;cs)
By
Latex:
(RWO "count-all" 0
THEN Auto'
THEN BLemma `l\_all\_iff`
THEN Auto
THEN RepeatFor 2 (D (-1))
THEN (InstHyp [\mkleeneopen{}i\mkleeneclose{}] (-7)\mcdot{} THENA Auto')
THEN SquashExRepD
THEN OnMaybeHyp 35 (\mbackslash{}h. ((InstHyp [\mkleeneopen{}k - 1\mkleeneclose{}] h\mcdot{} THENA Auto')
THEN (Subst' (r1 + 1) + (k - 1) \msim{} r1 + k -1 THEN Auto)
THEN FHyp (-1) [-3]
THEN Complete (Auto))))
Home
Index