---

Step * of Lemma new_23_sig_quorum_inv_vote2

∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀ni:ℤ × ℤ. ∀p:Cmd List × (Id List).
  (p ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e)
  ⇒ let cmds,locs = p 
     in no_repeats(Id;locs)
        ∧ (||locs|| = ||cmds|| ∈ ℤ)
        ∧ (∀i:ℕ||locs||
             (↓∃e':E
                ((e' <loc e)
                ∧ <<ni, cmds[i]>, locs[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
                ∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
                                             (¬<<ni, c>, locs[i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(
                                                                    e'')))))))
BY
{ MemoryInvariant }

1
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
⊢ ↓∃e':E
    ((e' <loc e)
    ∧ <<<n1, n2>, [a4 / s1][i]>, [a2 / s2][i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e')
    ∧ (∀e''∈[es-init(es;e);e').∀c:Cmd
                                 (¬<<<n1, n2>, c>, [a2 / s2][i]> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e''))))

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}notify,propose:Atom  List.  \mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).
\mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}ni:\mBbbZ{}  \mtimes{}  \mBbbZ{}.  \mforall{}p:Cmd  List  \mtimes{}  (Id  List).
    (p  \mmember{}  new\_23\_sig\_QuorumState(Cmd;notify;propose;f)  ni(e)
    {}\mRightarrow{}  let  cmds,locs  =  p 
          in  no\_repeats(Id;locs)
                \mwedge{}  (||locs||  =  ||cmds||)
                \mwedge{}  (\mforall{}i:\mBbbN{}||locs||
                          (\mdownarrow{}\mexists{}e':E
                                ((e'  <loc  e)
                                \mwedge{}  <<ni,  cmds[i]>,  locs[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{}<<ni,  c>,  locs[i]>  \mmember{}
                                                                                                new\_23\_sig\_vote'base(Cmd;notify;propose;f)(
                                                                                                e'')))))))


By

---

Latex:
MemoryInvariant

---

Home Index