---

Step * 1 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)
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
BY
{ (DVar `x'
   THEN ((RWO "assert_of_bnot" 11 THENM D 11)
         THENA (Auto THEN Try (OnSomeHyp(\i.(FLemma `new_23_sig_vote_with_ballot-assert-type` [i] THEN CpltAuto))⋅))
         )
   THEN ((BLemma `assert-bl-exists` THENM BLemma `l_exists_iff`)
         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 : E@i
10. (x ∈ [e, e'])@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
⊢ ∃x@0:E
   ((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)))))))

---

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)
14.  e1  :  E@i
15.  (e1  \mmember{}  [e;x))@i
16.  msgval(x)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id
17.  \muparrow{}new\_23\_sig\_vote\_with\_ballot\_and\_id(Cmd;notify;propose;f;es;e1;n;0;snd(msgval(x)))@i
\mvdash{}  False


By

---

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

---

Home Index