---

Step * of Lemma new_23_sig_agreement

∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify: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;eq;coeff;flrs;notify;propose;reps;slots;f)
  ⇒ bag-no-repeats(Id;reps)
  ⇒ (#(reps) = ((coeff * flrs) + flrs + 1) ∈ ℤ)
  ⇒ any v1,v2 from new_23_sig_decided'base(Cmd;notify;propose;f) satisfy
     ((fst(v1)) = (fst(v2)) ∈ ℤ) ⇒ ((snd(v1)) = (snd(v2)) ∈ Cmd))
BY
{ (Unfold `vatype` 0
   THEN Auto
   THEN AddMessageHeaderTypes
   THEN D 0
   THEN Auto
   THEN DProdsAndUnions
   THEN AllReduce
   THEN HypSubst' (-1) (-3)
   THEN ThinVar `v5'
   THEN RenameVar `n' (-4)
   THEN RenameVar `c1' (-5)
   THEN RenameVar `c2' (-3)
   THEN RepeatFor 2 ((FLemma `new_23_sig_decided_property` [-2;12] THENA Auto))
   THEN SquashExRepD) }

1
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'))
⊢ c1 = c2 ∈ Cmd

---

Latex:

---

Latex:
\mforall{}[Cmd:ValueAllType].  \mforall{}[eq:EqDecider(Cmd)].  \mforall{}[reps,clients:bag(Id)].  \mforall{}[coeff:\{2...\}].  \mforall{}[flrs:\mBbbN{}].
\mforall{}[propose,notify: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;eq;coeff;flrs;notify;propose;reps;slots;f)
    {}\mRightarrow{}  bag-no-repeats(Id;reps)
    {}\mRightarrow{}  (\#(reps)  =  ((coeff  *  flrs)  +  flrs  +  1))
    {}\mRightarrow{}  any  v1,v2  from  new\_23\_sig\_decided'base(Cmd;notify;propose;f)  satisfy
          ((fst(v1))  =  (fst(v2)))  {}\mRightarrow{}  ((snd(v1))  =  (snd(v2))))


By

---

Latex:
(Unfold  `vatype`  0
  THEN  Auto
  THEN  AddMessageHeaderTypes
  THEN  D  0
  THEN  Auto
  THEN  DProdsAndUnions
  THEN  AllReduce
  THEN  HypSubst'  (-1)  (-3)
  THEN  ThinVar  `v5'
  THEN  RenameVar  `n'  (-4)
  THEN  RenameVar  `c1'  (-5)
  THEN  RenameVar  `c2'  (-3)
  THEN  RepeatFor  2  ((FLemma  `new\_23\_sig\_decided\_property`  [-2;12]  THENA  Auto))
  THEN  SquashExRepD)

---

Home Index