---

Step * of Lemma new_23_sig_votes_consistent

∀[Cmd:ValueAllType]. ∀[cmdeq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff,flrs:ℤ]. ∀[notify,propose:Atom List].
∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)]. ∀[es:EO+(Message(f))].
  (new_23_sig_message-constraint{i:l}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)
  ⇒ (∀e1,e2:E. ∀n,r:ℤ. ∀sender,l1,l2:Id. ∀c1,c2:Cmd. ∀d1,d2:ℤ.
        (<d1, l1, make-Msg(``new_23_sig vote``;<<<n, r>, c1>, sender>)> ∈ new_23_sig_main()(e1)
        ⇒ <d2, l2, make-Msg(``new_23_sig vote``;<<<n, r>, c2>, sender>)> ∈ new_23_sig_main()(e2)
        ⇒ (c1 = c2 ∈ Cmd))))
BY
{ StartEmlProof }

1
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

---

Latex:

---

Latex:
\mforall{}[Cmd:ValueAllType].  \mforall{}[cmdeq:EqDecider(Cmd)].  \mforall{}[reps,clients:bag(Id)].  \mforall{}[coeff,flrs:\mBbbZ{}].
\mforall{}[notify,propose:Atom  List].  \mforall{}[slots:set-sig\{i:l\}(\mBbbZ{})].
\mforall{}[f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)].  \mforall{}[es:EO+(Message(f))].
    (new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;cmdeq;coeff;flrs;notify;propose;reps;slots;f)
    {}\mRightarrow{}  (\mforall{}e1,e2:E.  \mforall{}n,r:\mBbbZ{}.  \mforall{}sender,l1,l2:Id.  \mforall{}c1,c2:Cmd.  \mforall{}d1,d2:\mBbbZ{}.
                (<d1,  l1,  make-Msg(``new\_23\_sig  vote``;<<<n,  r>,  c1>,  sender>)>  \mmember{}  new\_23\_sig\_main()(e1)
                {}\mRightarrow{}  <d2,  l2,  make-Msg(``new\_23\_sig  vote``;<<<n,  r>,  c2>,  sender>)>  \mmember{}  new\_23\_sig\_main()(e2)
                {}\mRightarrow{}  (c1  =  c2))))


By

---

Latex:
StartEmlProof

---

Home Index