---

Step * 1 2 1 of Lemma filter-vote-with-ballot-lemma


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. n : ℤ@i
8. e' : E@i
9. x : {x:E| (x ∈ [e, e'])} @i
10. ↑(∀e'∈[e;x).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;0;snd(msgval(x))))_b@i
11. ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x;n;0)
12. new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x;n;0) = tt
13. has-es-info-type(es;x;f;ℤ × ℤ × Cmd × Id)
14. x@0 : E
15. (x@0 ∈ [e, e'])
16. ↑(new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x@0;n;0)
∧b es-blocl(es;x@0;x)
∧b (IdDeq (snd(msgval(x@0))) (snd(msgval(x)))))
⊢ False
BY
{ ((BoolCase ⌈new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x@0;n;0)⌉⋅ THENA Auto)
   THEN (FLemma `new_23_sig_vote_with_ballot-assert-type` [-1] THENA Auto)
   ) }

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. es : EO+(Message(f))@i'
6. e : E@i
7. n : ℤ@i
8. e' : E@i
9. x : {x:E| (x ∈ [e, e'])} @i
10. ↑(∀e'∈[e;x).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;0;snd(msgval(x))))_b@i
11. ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x;n;0)
12. new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x;n;0) = tt
13. has-es-info-type(es;x;f;ℤ × ℤ × Cmd × Id)
14. x@0 : E
15. (x@0 ∈ [e, e'])
16. ↑(new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x@0;n;0)
∧b es-blocl(es;x@0;x)
∧b (IdDeq (snd(msgval(x@0))) (snd(msgval(x)))))
17. ↑new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x@0;n;0)
18. has-es-info-type(es;x@0;f;ℤ × ℤ × Cmd × Id)
⊢ False

---

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.  n  :  \mBbbZ{}@i
8.  e'  :  E@i
9.  x  :  \{x:E|  (x  \mmember{}  [e,  e'])\}  @i
10.  \muparrow{}(\mforall{}e'\mmember{}[e;x).
                  \mneg{}\msubb{}new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e';n;0;snd(msgval(x))))\_b@i
11.  \muparrow{}new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;x;n;0)
12.  new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;x;n;0)  =  tt
13.  has-es-info-type(es;x;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
14.  x@0  :  E
15.  (x@0  \mmember{}  [e,  e'])
16.  \muparrow{}(new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;x@0;n;0)
\mwedge{}\msubb{}  es-blocl(es;x@0;x)
\mwedge{}\msubb{}  (IdDeq  (snd(msgval(x@0)))  (snd(msgval(x)))))
\mvdash{}  False


By

---

Latex:
((BoolCase  \mkleeneopen{}new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;x@0;n;0)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (FLemma  `new\_23\_sig\_vote\_with\_ballot-assert-type`  [-1]  THENA  Auto)
  )

---

Home Index