---

Step * 1 1 of Lemma new_23_sig_vote_with_ballot_first-assert-forward2


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. es : EO+(Message(f))@i'
6. e : E@i
7. start : E@i
8. n : ℤ@i
9. r : ℤ@i
10. start ≤loc e @i
11. ↑(new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
∧b (∀e'∈[start;e).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))_b)@i
12. ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;e;n;r)
13. has-es-info-type(es;e;f;ℤ × ℤ × Cmd × Id)
⊢ (∀e'∈[start;e).¬↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))
BY
{ (RW assert_pushdownC (-3) THEN Auto)⋅ }

---

Latex:

---

Latex:

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.  es  :  EO+(Message(f))@i'
6.  e  :  E@i
7.  start  :  E@i
8.  n  :  \mBbbZ{}@i
9.  r  :  \mBbbZ{}@i
10.  start  \mleq{}loc  e  @i
11.  \muparrow{}(new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;e;n;r)
\mwedge{}\msubb{}  (\mforall{}e'\mmember{}[start;e).
              \mneg{}\msubb{}new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))\_b)@i
12.  \muparrow{}new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;e;n;r)
13.  has-es-info-type(es;e;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
\mvdash{}  (\mforall{}e'\mmember{}[start;e).
            \mneg{}\muparrow{}new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e';n;r;snd(msgval(e))))


By

---

Latex:
(RW  assert\_pushdownC  (-3)  THEN  Auto)\mcdot{}

---

Home Index