Step
*
1
2
1
of Lemma
new_23_sig_agreement
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. c1 : Cmd@i
24. n : ℤ@i
25. c2 : Cmd@i
26. <n, c1> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)@i
27. <n, c2> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e2)@i
28. x1 : Id
29. r1 : ℕ
30. L1 : Id List
31. no_repeats(Id;L1)
32. ||L1|| = ((coeff * flrs) + 1) ∈ ℤ
33. (∀vtr∈L1.↓∃e':E. mk-msg-interface(x1;make-Msg(``new_23_sig vote``;<<<n, r1>, c1>, vtr>)) ∈ new_23_sig_main()(e'))
34. x : Id
35. rnd : ℕ
36. L : Id List
37. no_repeats(Id;L)
38. ||L|| = ((coeff * flrs) + 1) ∈ ℤ
39. (∀vtr∈L.↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, rnd>, c2>, vtr>)) ∈ new_23_sig_main()(e'))
40. ¬(r1 = rnd ∈ ℤ)
41. 0 ≤ (coeff * flrs)
42. r1 < rnd
⊢ c1 = c2 ∈ Cmd
BY
{ Assert ⌈∀k:ℕ. ∀e':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()(e') ⇒ (c = c1 ∈ Cmd))⌉⋅ }
1
.....assertion.....
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. c1 : Cmd@i
24. n : ℤ@i
25. c2 : Cmd@i
26. <n, c1> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)@i
27. <n, c2> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e2)@i
28. x1 : Id
29. r1 : ℕ
30. L1 : Id List
31. no_repeats(Id;L1)
32. ||L1|| = ((coeff * flrs) + 1) ∈ ℤ
33. (∀vtr∈L1.↓∃e':E. mk-msg-interface(x1;make-Msg(``new_23_sig vote``;<<<n, r1>, c1>, vtr>)) ∈ new_23_sig_main()(e'))
34. x : Id
35. rnd : ℕ
36. L : Id List
37. no_repeats(Id;L)
38. ||L|| = ((coeff * flrs) + 1) ∈ ℤ
39. (∀vtr∈L.↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, rnd>, c2>, vtr>)) ∈ new_23_sig_main()(e'))
40. ¬(r1 = rnd ∈ ℤ)
41. 0 ≤ (coeff * flrs)
42. r1 < rnd
⊢ ∀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_23\000C_sig_main()(e') ⇒ (c = c1 ∈ Cmd))
2
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. c1 : Cmd@i
24. n : ℤ@i
25. c2 : Cmd@i
26. <n, c1> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)@i
27. <n, c2> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e2)@i
28. x1 : Id
29. r1 : ℕ
30. L1 : Id List
31. no_repeats(Id;L1)
32. ||L1|| = ((coeff * flrs) + 1) ∈ ℤ
33. (∀vtr∈L1.↓∃e':E. mk-msg-interface(x1;make-Msg(``new_23_sig vote``;<<<n, r1>, c1>, vtr>)) ∈ new_23_sig_main()(e'))
34. x : Id
35. rnd : ℕ
36. L : Id List
37. no_repeats(Id;L)
38. ||L|| = ((coeff * flrs) + 1) ∈ ℤ
39. (∀vtr∈L.↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, rnd>, c2>, vtr>)) ∈ new_23_sig_main()(e'))
40. ¬(r1 = rnd ∈ ℤ)
41. 0 ≤ (coeff * flrs)
42. r1 < rnd
43. ∀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_\000C23_sig_main()(e') ⇒ (c = c1 ∈ Cmd))
⊢ c1 = c2 ∈ Cmd
Latex:
Latex:
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. c1 : Cmd@i
24. n : \mBbbZ{}@i
25. c2 : Cmd@i
26. <n, c1> \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e1)@i
27. <n, c2> \mmember{} new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e2)@i
28. x1 : Id
29. r1 : \mBbbN{}
30. L1 : Id List
31. no\_repeats(Id;L1)
32. ||L1|| = ((coeff * flrs) + 1)
33. (\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'))
34. x : Id
35. rnd : \mBbbN{}
36. L : Id List
37. no\_repeats(Id;L)
38. ||L|| = ((coeff * flrs) + 1)
39. (\mforall{}vtr\mmember{}L.\mdownarrow{}\mexists{}e':E. mk-msg-interface(x;make-Msg(``new\_23\_sig vote``;<<<n, rnd>, c2>, vtr>)) \mmember{} new\_23\000C\_sig\_main()(e'))
40. \mneg{}(r1 = rnd)
41. 0 \mleq{} (coeff * flrs)
42. r1 < rnd
\mvdash{} c1 = c2
By
Latex:
Assert \mkleeneopen{}\mforall{}k:\mBbbN{}. \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\_si\000Cg\_main()(e') {}\mRightarrow{} (c = c1))\mkleeneclose{}\mcdot{}
Home
Index