---

Step * 1 1 of Lemma new_23_sig_quorum_mem


1. Cmd : {T:Type| valueall-type(T)} @i'
2. notify : Atom List@i
3. propose : Atom List@i
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)@i'
5. (f propose) = (ℤ × Cmd) ∈ Type
6. (f notify) = (ℤ × Cmd) ∈ Type
7. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
8. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
9. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
10. f ∈ Name ─→ Type
11. es : EO+(Message(f))@i'
12. e1 : E@i
13. e2 : E@i
14. n1 : ℤ@i
15. n2 : ℤ@i
16. s7 : Cmd List@i
17. s8 : Id List@i
18. s5 : Cmd List@i
19. s6 : Id List@i
20. v5 : ℤ@i
21. v6 : ℤ@i
22. v4 : Cmd@i
23. v2 : Id@i
24. (e1 <loc e2)@i
25. <<<v5, v6>, v4>, v2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)@i
26. <s7, s8> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e1)
27. <s5, s6> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e2)
28. a5 : ℤ@i
29. a6 : ℤ@i
30. a4 : Cmd@i
31. a2 : Id@i
32. s3 : Cmd List@i
33. s4 : Id List@i
34. ¬¬(a2 ∈ s4)
35. e : E@i
36. e1 ≤loc e @i
37. (e <loc e2)@i
38. <<<a5, a6>, a4>, a2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)@i
39. <s3, s4> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e)@i
40. n1 = a5 ∈ ℤ
41. n2 = a6 ∈ ℤ
⊢ (a2 ∈ s4)
BY
{ SupposeNot }

---

Latex:

---

Latex:

1.  Cmd  :  \{T:Type|  valueall-type(T)\}  @i'
2.  notify  :  Atom  List@i
3.  propose  :  Atom  List@i
4.  f  :  new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)@i'
5.  (f  propose)  =  (\mBbbZ{}  \mtimes{}  Cmd)
6.  (f  notify)  =  (\mBbbZ{}  \mtimes{}  Cmd)
7.  (f  ``new\_23\_sig  decided``)  =  (\mBbbZ{}  \mtimes{}  Cmd)
8.  (f  ``new\_23\_sig  retry``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
9.  (f  ``new\_23\_sig  vote``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
10.  f  \mmember{}  Name  {}\mrightarrow{}  Type
11.  es  :  EO+(Message(f))@i'
12.  e1  :  E@i
13.  e2  :  E@i
14.  n1  :  \mBbbZ{}@i
15.  n2  :  \mBbbZ{}@i
16.  s7  :  Cmd  List@i
17.  s8  :  Id  List@i
18.  s5  :  Cmd  List@i
19.  s6  :  Id  List@i
20.  v5  :  \mBbbZ{}@i
21.  v6  :  \mBbbZ{}@i
22.  v4  :  Cmd@i
23.  v2  :  Id@i
24.  (e1  <loc  e2)@i
25.  <<<v5,  v6>,  v4>,  v2>  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e1)@i
26.  <s7,  s8>  \mmember{}  Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)  <n1,  n2>\mlambda{}loc.\{<[],  []>\};new\_23\_sig\_vo\000Cte'base(Cmd;notify;propose;f))(
                              e1)
27.  <s5,  s6>  \mmember{}  Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)  <n1,  n2>\mlambda{}loc.\{<[],  []>\};new\_23\_sig\_vo\000Cte'base(Cmd;notify;propose;f))(
                              e2)
28.  a5  :  \mBbbZ{}@i
29.  a6  :  \mBbbZ{}@i
30.  a4  :  Cmd@i
31.  a2  :  Id@i
32.  s3  :  Cmd  List@i
33.  s4  :  Id  List@i
34.  \mneg{}\mneg{}(a2  \mmember{}  s4)
35.  e  :  E@i
36.  e1  \mleq{}loc  e  @i
37.  (e  <loc  e2)@i
38.  <<<a5,  a6>,  a4>,  a2>  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e)@i
39.  <s3,  s4>  \mmember{}  Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd)  <n1,  n2>\mlambda{}loc.\{<[],  []>\};new\_23\_sig\_vo\000Cte'base(Cmd;notify;propose;f))(
                              e)@i
40.  n1  =  a5
41.  n2  =  a6
\mvdash{}  (a2  \mmember{}  s4)


By

---

Latex:
SupposeNot

---

Home Index