---

Step * of Lemma new_23_sig_vote_with_ballot_first-not

∀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:ℤ.
  ((∃e'∈[es-init(es;e);e). ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(...)))) supposing 
     ((¬↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es;e;n;r)) and 
     (↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)))
BY
{ Seq [ Try (Unfold `vatype` 0)
      ; Auto
      ; Try (AddMessageHeaderTypes
             THEN RepeatFor 2 (MoveToHeaderType (-1)))
      ]⋅ }

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)
∧ ((f notify) = (ℤ × Cmd) ∈ Type)
∧ ((f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type)
∧ ((f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type)
∧ ((f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type)
6. f ∈ Name ─→ Type
7. es : EO+(Message(f))@i'
8. e : E@i
9. n : ℤ@i
10. r : ℤ@i
11. ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
12. ¬↑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;snd(msgval(e))))

---

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{}.
    ((\mexists{}e'\mmember{}[es-init(es;e);e).  \muparrow{}...))  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(Cmd;notify;propose;f;es;e;n;r)))


By

---

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

---

Home Index