---

Step * 1 1 1 of Lemma new_23_sig_quorum_inv_vote2


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. e : E@i
13. n1 : ℤ@i
14. n2 : ℤ@i
15. p1 : Cmd List@i
16. p2 : Id List@i
17. <p1, p2> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e)
18. a5 : ℤ@i
19. a6 : ℤ@i
20. a4 : Cmd@i
21. a2 : Id@i
22. e' : E@i
23. s1 : Cmd List@i
24. s2 : Id List@i
25. (e' <loc e)@i
26. <<<a5, a6>, a4>, a2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')@i
27. <s1, s2> ∈ 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
28. no_repeats(Id;s2)@i
29. ||s2|| = ||s1|| ∈ ℤ@i
30. ∀i:ℕ||s2||
      (↓∃e':E
         ((e' <loc e)
         ∧ <<<n1, n2>, s1[i]>, s2[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
         ∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
                                      (¬<<<n1, n2>, c>, s2[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e'')))))@i
31. n1 = a5 ∈ ℤ
32. n2 = a6 ∈ ℤ
33. ¬(a2 ∈ s2)
34. i : ℕ||s2|| + 1@i
35. i = 0 ∈ ℤ
36. (e' <loc e)
37. <<<n1, n2>, a4>, a2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
38. e'' : E@i
39. (e'' ∈ [es-init(es;e);e'))@i
40. c : Cmd@i
41. <<<n1, n2>, c>, a2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e'')@i
⊢ False
BY
{ ((Assert ⌈<s1, s2> ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) <n1, n2>(e')⌉⋅ THENA (ReduceToOldState 10 0 THEN Tri\000Cvial⋅))
   THEN (InstLemma `new_23_sig_quorum_mem` [⌈Cmd⌉;⌈notify⌉;⌈propose⌉;⌈f⌉;⌈es⌉;⌈e''⌉;⌈e'⌉;⌈<n1, n2>⌉;
         ⌈new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n1, n2>;es;e'')⌉;⌈<s1, s2>⌉;⌈<<<n1, n2>, c>, a2>⌉]⋅
         THENA (Auto THEN Try ((RW ListC (-4) THEN Auto)) THEN BLemma `new_23_sig_QuorumState-classrel` THEN Auto)
         )
   THEN UsePairEta [1] (-1)
   THEN D (-1)
   THEN Auto) }

---

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.  e  :  E@i
13.  n1  :  \mBbbZ{}@i
14.  n2  :  \mBbbZ{}@i
15.  p1  :  Cmd  List@i
16.  p2  :  Id  List@i
17.  <p1,  p2>  \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)
18.  a5  :  \mBbbZ{}@i
19.  a6  :  \mBbbZ{}@i
20.  a4  :  Cmd@i
21.  a2  :  Id@i
22.  e'  :  E@i
23.  s1  :  Cmd  List@i
24.  s2  :  Id  List@i
25.  (e'  <loc  e)@i
26.  <<<a5,  a6>,  a4>,  a2>  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')@i
27.  <s1,  s2>  \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
28.  no\_repeats(Id;s2)@i
29.  ||s2||  =  ||s1||@i
30.  \mforall{}i:\mBbbN{}||s2||
            (\mdownarrow{}\mexists{}e':E
                  ((e'  <loc  e)
                  \mwedge{}  <<<n1,  n2>,  s1[i]>,  s2[i]>  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')
                  \mwedge{}  (\mforall{}e''\mmember{}[es-init(es;e);e').\mforall{}c:Cmd
                                                                            (\mneg{}<<<n1,  n2>,  c>,  s2[i]>  \mmember{}
                                                                                  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e'')))))@i
31.  n1  =  a5
32.  n2  =  a6
33.  \mneg{}(a2  \mmember{}  s2)
34.  i  :  \mBbbN{}||s2||  +  1@i
35.  i  =  0
36.  (e'  <loc  e)
37.  <<<n1,  n2>,  a4>,  a2>  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e')
38.  e''  :  E@i
39.  (e''  \mmember{}  [es-init(es;e);e'))@i
40.  c  :  Cmd@i
41.  <<<n1,  n2>,  c>,  a2>  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e'')@i
\mvdash{}  False


By

---

Latex:
((Assert  \mkleeneopen{}<s1,  s2>  \mmember{}  new\_23\_sig\_QuorumState(Cmd;notify;propose;f)  <n1,  n2>(e')\mkleeneclose{}\mcdot{}  THENA  (ReduceToOldS\000Ctate  10  0  THEN  Trivial\mcdot{}))
  THEN  (InstLemma  `new\_23\_sig\_quorum\_mem`  [\mkleeneopen{}Cmd\mkleeneclose{};\mkleeneopen{}notify\mkleeneclose{};\mkleeneopen{}propose\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}es\mkleeneclose{};\mkleeneopen{}e''\mkleeneclose{};\mkleeneopen{}e'\mkleeneclose{};\mkleeneopen{}<n1,  n2>\mkleeneclose{};
              \mkleeneopen{}new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n1,  n2>es;e'')\mkleeneclose{};\mkleeneopen{}<s1,  s2>\mkleeneclose{};\mkleeneopen{}<<<n1,  n2>,  c>,\000C  a2>\mkleeneclose{}]\mcdot{}
              THENA  (Auto
                            THEN  Try  ((RW  ListC  (-4)  THEN  Auto))
                            THEN  BLemma  `new\_23\_sig\_QuorumState-classrel`
                            THEN  Auto)
              )
  THEN  UsePairEta  [1]  (-1)
  THEN  D  (-1)
  THEN  Auto)

---

Home Index