---

Step * 1 of Lemma new_23_sig_votes_consistent


1. Cmd : {T:Type| valueall-type(T)} 
2. cmdeq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : ℤ
6. flrs : ℤ
7. notify : Atom List
8. propose : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. (f propose) = (ℤ × Cmd) ∈ Type
12. (f notify) = (ℤ × Cmd) ∈ Type
13. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
15. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
16. f ∈ Name ─→ Type
17. es : EO+(Message(f))
18. new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@i'
19. e1 : E@i
20. e2 : E@i
21. n : ℤ@i
22. r : ℤ@i
23. sender : Id@i
24. l1 : Id@i
25. l2 : Id@i
26. c1 : Cmd@i
27. c2 : Cmd@i
28. d1 : ℤ@i
29. d2 : ℤ@i
30. <d1, l1, make-Msg(``new_23_sig vote``;<<<n, r>, c1>, sender>)> ∈ new_23_sig_main()(e1)@i
31. <d2, l2, make-Msg(``new_23_sig vote``;<<<n, r>, c2>, sender>)> ∈ new_23_sig_main()(e2)@i
⊢ c1 = c2 ∈ Cmd
BY
{ (All (\h. (Unfold `make-Msg` h THEN Fold `mk-msg` h THEN (RWO "new_23_sig-vote" h THENA Auto)))⋅
   THEN SquashExRepD
   THEN DVarSets) }

1
1. Cmd : Type
2. valueall-type(Cmd)
3. cmdeq : EqDecider(Cmd)
4. reps : bag(Id)
5. clients : bag(Id)
6. coeff : ℤ
7. flrs : ℤ
8. notify : Atom List
9. propose : Atom List
10. slots : set-sig{i:l}(ℤ)
11. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
12. (f propose) = (ℤ × Cmd) ∈ Type
13. (f notify) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
15. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
16. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
17. f ∈ Name ─→ Type
18. es : EO+(Message(f))
19. new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@i'
20. e1 : E@i
21. e2 : E@i
22. n : ℤ@i
23. r : ℤ@i
24. sender : Id@i
25. l1 : Id@i
26. l2 : Id@i
27. c1 : Cmd@i
28. c2 : Cmd@i
29. d1 : ℤ@i
30. d2 : ℤ@i
31. loc(e1) ↓∈ reps
32. e3 : E
33. e3 ≤loc e1 
34. z3 : Cmd
35. ((header(e3) = propose ∈ Name) ∧ has-es-info-type(es;e3;f;ℤ × Cmd) ∧ (<n, z3> = 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))))) ∈ ℤ)
  ∧ (z3 = (snd(fst(msgval(e3)))) ∈ Cmd))
36. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e3))
37. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e3 and e1)
38. l1 ↓∈ reps
39. d1 = 0 ∈ ℤ
40. ff = ff
41. sender = loc(e1) ∈ Id
42. ((r = 0 ∈ ℤ) ∧ (c1 = z3 ∈ Cmd) ∧ (e1 = e3 ∈ E))
∨ (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e3;e1) < r
  ∧ (((header(e1) = ``new_23_sig retry`` ∈ Name)
    ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd)
    ∧ (<<n, r>, c1> = msgval(e1) ∈ (ℤ × ℤ × Cmd)))
    ∨ ((header(e1) = ``new_23_sig vote`` ∈ Name)
      ∧ has-es-info-type(es;e1;f;ℤ × ℤ × Cmd × Id)
      ∧ (<<n, r>, c1> = (fst(msgval(e1))) ∈ (ℤ × ℤ × Cmd)))))
43. loc(e2) ↓∈ reps
44. e' : E
45. e' ≤loc e2 
46. z2 : Cmd
47. ((header(e') = propose ∈ Name) ∧ has-es-info-type(es;e';f;ℤ × Cmd) ∧ (<n, z2> = msgval(e') ∈ (ℤ × Cmd)))
∨ ((header(e') = ``new_23_sig vote`` ∈ Name)
  ∧ has-es-info-type(es;e';f;ℤ × ℤ × Cmd × Id)
  ∧ (n = (fst(fst(fst(msgval(e'))))) ∈ ℤ)
  ∧ (z2 = (snd(fst(msgval(e')))) ∈ Cmd))
48. ¬↑(set-sig-member(slots) n new_23_sig_ReplicaStateFun(Cmd;notify;propose;slots;f;es;e'))
49. (no new_23_sig_Notify(Cmd;clients;notify;propose;f) n between e' and e2)
50. l2 ↓∈ reps
51. d2 = 0 ∈ ℤ
52. ff = ff
53. sender = loc(e2) ∈ Id
54. ((r = 0 ∈ ℤ) ∧ (c2 = z2 ∈ Cmd) ∧ (e2 = e' ∈ E))
∨ (new_23_sig_NewRoundsStateFun(Cmd;notify;propose;f;n;es.e';e2) < r
  ∧ (((header(e2) = ``new_23_sig retry`` ∈ Name)
    ∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd)
    ∧ (<<n, r>, c2> = msgval(e2) ∈ (ℤ × ℤ × Cmd)))
    ∨ ((header(e2) = ``new_23_sig vote`` ∈ Name)
      ∧ has-es-info-type(es;e2;f;ℤ × ℤ × Cmd × Id)
      ∧ (<<n, r>, c2> = (fst(msgval(e2))) ∈ (ℤ × ℤ × Cmd)))))
⊢ c1 = c2 ∈ Cmd

---

Latex:

---

Latex:

1.  Cmd  :  \{T:Type|  valueall-type(T)\} 
2.  cmdeq  :  EqDecider(Cmd)
3.  reps  :  bag(Id)
4.  clients  :  bag(Id)
5.  coeff  :  \mBbbZ{}
6.  flrs  :  \mBbbZ{}
7.  notify  :  Atom  List
8.  propose  :  Atom  List
9.  slots  :  set-sig\{i:l\}(\mBbbZ{})
10.  f  :  new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)
11.  (f  propose)  =  (\mBbbZ{}  \mtimes{}  Cmd)
12.  (f  notify)  =  (\mBbbZ{}  \mtimes{}  Cmd)
13.  (f  ``new\_23\_sig  decided``)  =  (\mBbbZ{}  \mtimes{}  Cmd)
14.  (f  ``new\_23\_sig  retry``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
15.  (f  ``new\_23\_sig  vote``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
16.  f  \mmember{}  Name  {}\mrightarrow{}  Type
17.  es  :  EO+(Message(f))
18.  new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)@i'
19.  e1  :  E@i
20.  e2  :  E@i
21.  n  :  \mBbbZ{}@i
22.  r  :  \mBbbZ{}@i
23.  sender  :  Id@i
24.  l1  :  Id@i
25.  l2  :  Id@i
26.  c1  :  Cmd@i
27.  c2  :  Cmd@i
28.  d1  :  \mBbbZ{}@i
29.  d2  :  \mBbbZ{}@i
30.  <d1,  l1,  make-Msg(``new\_23\_sig  vote``;<<<n,  r>,  c1>,  sender>)>  \mmember{}  new\_23\_sig\_main()(e1)@i
31.  <d2,  l2,  make-Msg(``new\_23\_sig  vote``;<<<n,  r>,  c2>,  sender>)>  \mmember{}  new\_23\_sig\_main()(e2)@i
\mvdash{}  c1  =  c2


By

---

Latex:
(All  (\mbackslash{}h.  (Unfold  `make-Msg`  h  THEN  Fold  `mk-msg`  h  THEN  (RWO  "new\_23\_sig-vote"  h  THENA  Auto)))\mcdot{}
  THEN  SquashExRepD
  THEN  DVarSets)

---

Home Index