---

Step * 1 2 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)
⊢ ↑¬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
BY
{ ((BLemma `assert_of_bnot` THENM RWO "assert-bl-exists" 0 THENM D 0 THENM RWO "l_exists_iff" (-1) THENM ExRepD)
   THENA (Auto THEN Try (OnSomeHyp(\i.(FLemma `new_23_sig_vote_with_ballot-assert-type` [i] THEN CpltAuto))⋅))
   ) }

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)))))
⊢ 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)
\mvdash{}  \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


By

---

Latex:
((BLemma  `assert\_of\_bnot`
    THENM  RWO  "assert-bl-exists"  0
    THENM  D  0
    THENM  RWO  "l\_exists\_iff"  (-1)
    THENM  ExRepD)
  THENA  (Auto
                THEN  Try  (OnSomeHyp(\mbackslash{}i.(FLemma  `new\_23\_sig\_vote\_with\_ballot-assert-type`  [i]  THEN  CpltAuto))
                                    \mcdot{})
                )
  )

---

Home Index