---

Step * 1 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. ↑¬b(∃x@0∈[e, e'].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)))))_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)
⊢ ↑(∀e'∈[e;x).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;0;snd(msgval(x))))_b
BY
{ ((BLemma `assert-bl-all` THENA Auto) THEN RWO "l_all_iff" 0 THEN Auto THEN (D 0 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. ↑¬b(∃x@0∈[e, e'].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)))))_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. e1 : E@i
15. (e1 ∈ [e;x))@i
16. msgval(x) ∈ ℤ × ℤ × Cmd × Id
17. ↑new_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e1;n;0;snd(msgval(x)))@i
⊢ 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{}\mneg{}\msubb{}(\mexists{}x@0\mmember{}[e,  e'].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)))))\_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)
\mvdash{}  \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


By

---

Latex:
((BLemma  `assert-bl-all`  THENA  Auto)  THEN  RWO  "l\_all\_iff"  0  THEN  Auto  THEN  (D  0  THENA  Auto))

---

Home Index