---

Step * of Lemma new_23_sig_vote_with_ballot_first-not2

∀Cmd:ValueAllType. ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e:E. ∀n,r:ℤ. ∀i:Id.
  ((∃e'∈[es-init(es;e);e). (↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;i))
     ∧ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e';n;r)))) supposing 
     ((¬↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)) and 
     (↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)))
BY
{ Seq [ Try (Unfold `vatype` 0)
      ; Auto
      ; Try (AddMessageHeaderTypes
             THEN RepeatFor 2 (MoveToHeaderType (-1)))

      ; RepD
      ]⋅ }

1
1. Cmd : {T:Type| valueall-type(T)} @i'
2. propose : Atom List@i
3. notify : 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. n : ℤ@i
14. r : ℤ@i
15. i : Id@i
16. ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e;n;r;i)
17. ¬↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)
⊢ (∃e'∈[es-init(es;e);e). (↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;i))
∧ (↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e';n;r)))

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}propose,notify:Atom  List.  \mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).
\mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}n,r:\mBbbZ{}.  \mforall{}i:Id.
    ((\mexists{}e'\mmember{}[es-init(es;e);e).  (\muparrow{}new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e';n;r;i))
          \mwedge{}  (\muparrow{}new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e';n;r))))  supposing 
          ((\mneg{}\muparrow{}new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es;e;n;r))  and 
          (\muparrow{}new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e;n;r;i)))


By

---

Latex:
Seq  [  Try  (Unfold  `vatype`  0)
            ;  Auto
            ;  Try  (AddMessageHeaderTypes
                          THEN  RepeatFor  2  (MoveToHeaderType  (-1)))

            ;  RepD
            ]\mcdot{}

---

Home Index