---

Step * 1 2 2 2 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. c2 : Cmd@i
24. n : ℤ@i
25. c1 : Cmd@i
26. <n, c2> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e1)@i
27. <n, c1> ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e2)@i
28. x : Id
29. rnd : ℕ
30. L : Id List
31. no_repeats(Id;L)
32. ||L|| = ((coeff * flrs) + 1) ∈ ℤ
33. (∀vtr∈L.↓∃e':E. mk-msg-interface(x;make-Msg(``new_23_sig vote``;<<<n, rnd>, c2>, vtr>)) ∈ new_23_sig_main()(e'))
34. x1 : Id
35. r1 : ℕ
36. L1 : Id List
37. no_repeats(Id;L1)
38. ||L1|| = ((coeff * flrs) + 1) ∈ ℤ
39. (∀vtr∈L1.↓∃e':E. mk-msg-interface(x1;make-Msg(``new_23_sig vote``;<<<n, r1>, c1>, vtr>)) ∈ new_23_sig_main()(e'))
40. ¬(rnd = r1 ∈ ℤ)
41. 0 ≤ (coeff * flrs)
42. ¬rnd < r1
43. r1 < rnd
44. ∀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))
⊢ c2 = c1 ∈ Cmd
BY
{ ((Assert ¬↑null(L) BY
          (DVar `L' THEN All Reduce THEN Auto'))
   THEN All(\i.(RWO "l_all_iff" i THENA (Auto THEN Assert ⌈(ℤ × ℕ × Cmd × Id) ⊆r (ℤ × ℤ × Cmd × Id)⌉⋅ THEN Auto)))⋅
   THEN (With ⌈hd(L)⌉ (D (-13))⋅ THENA (Auto THEN Auto'))
   THEN ((D -1 THENM SquashExRepD) THENA (Auto THEN GenListD 0))
   THEN InstHyp [⌈rnd - r1 + 1⌉;⌈e'⌉;⌈x⌉;⌈hd(L)⌉;⌈c2⌉] (-4)⋅
   THEN Auto') }

---

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.  c2  :  Cmd@i
24.  n  :  \mBbbZ{}@i
25.  c1  :  Cmd@i
26.  <n,  c2>  \mmember{}  new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e1)@i
27.  <n,  c1>  \mmember{}  new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e2)@i
28.  x  :  Id
29.  rnd  :  \mBbbN{}
30.  L  :  Id  List
31.  no\_repeats(Id;L)
32.  ||L||  =  ((coeff  *  flrs)  +  1)
33.  (\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'))
34.  x1  :  Id
35.  r1  :  \mBbbN{}
36.  L1  :  Id  List
37.  no\_repeats(Id;L1)
38.  ||L1||  =  ((coeff  *  flrs)  +  1)
39.  (\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'))
40.  \mneg{}(rnd  =  r1)
41.  0  \mleq{}  (coeff  *  flrs)
42.  \mneg{}rnd  <  r1
43.  r1  <  rnd
44.  \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\_sig\_ma\000Cin()(e')  {}\mRightarrow{}  (c  =  c1))
\mvdash{}  c2  =  c1


By

---

Latex:
((Assert  \mneg{}\muparrow{}null(L)  BY
                (DVar  `L'  THEN  All  Reduce  THEN  Auto'))
  THEN  All(\mbackslash{}i.(RWO  "l\_all\_iff"  i
                            THENA  (Auto  THEN  Assert  \mkleeneopen{}(\mBbbZ{}  \mtimes{}  \mBbbN{}  \mtimes{}  Cmd  \mtimes{}  Id)  \msubseteq{}r  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)\mkleeneclose{}\mcdot{}  THEN  Auto)
                            ))\mcdot{}
  THEN  (With  \mkleeneopen{}hd(L)\mkleeneclose{}  (D  (-13))\mcdot{}  THENA  (Auto  THEN  Auto'))
  THEN  ((D  -1  THENM  SquashExRepD)  THENA  (Auto  THEN  GenListD  0))
  THEN  InstHyp  [\mkleeneopen{}rnd  -  r1  +  1\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}hd(L)\mkleeneclose{};\mkleeneopen{}c2\mkleeneclose{}]  (-4)\mcdot{}
  THEN  Auto')

---

Home Index