---

Step * 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
⊢ filter(λa.new_23_sig_vote_with_ballot_first_alt(Cmd;notify;propose;f;es;e;e';n;0;a);[e, e']) 
~ filter(λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;0);[e, e'])
BY
{ (BLemma `filter-sq`⋅
   THEN Auto
   THEN Try (Complete ((RW ListC (-2) THEN Auto)))
   THEN Try (Complete ((D (-2) THEN Unhide THEN Auto THEN RW ListC (-2) THEN Auto)))
   THEN Reduce (-1)
   THEN (All(RWO "new_23_sig_vote_with_ballot_first-forward") THENA Auto)
   THEN (Try (Complete ((D (-2) THEN Unhide THEN Auto THEN RW ListC (-2) THEN Auto)))
         THEN (RepUR ``new_23_sig_vote_with_ballot_first_alt`` 0
               THEN RepUR ``new_23_sig_vote_with_ballot_first_alt`` -1
               )
         THEN (BoolCase ⌈new_23_sig_vote_with_ballot(Cmd;notify;propose;f;es;x;n;0)⌉⋅ THENA Auto)
         THEN (DupHyp (-1)
               THEN (RWO "eqtt_to_assert<" (-1) THENA Auto)
               THEN (HypSubst' (-1) (-3) THEN Reduce (-3))
               THEN (FLemma `new_23_sig_vote_with_ballot-assert-type` [-2] 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)
⊢ ↑(∀e'∈[e;x).¬bnew_23_sig_vote_with_ballot_and_id(Cmd;notify;propose;f;es;e';n;0;snd(msgval(x))))_b

2
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

---

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
\mvdash{}  filter(\mlambda{}a.new\_23\_sig\_vote\_with\_ballot\_first\_alt(Cmd;notify;propose;f;es;e;e';n;0;a);[e,  e']) 
\msim{}  filter(\mlambda{}e'.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es.e;e';n;0);[e,  e'])


By

---

Latex:
(BLemma  `filter-sq`\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((RW  ListC  (-2)  THEN  Auto)))
  THEN  Try  (Complete  ((D  (-2)  THEN  Unhide  THEN  Auto  THEN  RW  ListC  (-2)  THEN  Auto)))
  THEN  Reduce  (-1)
  THEN  (All(RWO  "new\_23\_sig\_vote\_with\_ballot\_first-forward")  THENA  Auto)
  THEN  (Try  (Complete  ((D  (-2)  THEN  Unhide  THEN  Auto  THEN  RW  ListC  (-2)  THEN  Auto)))
              THEN  (RepUR  ``new\_23\_sig\_vote\_with\_ballot\_first\_alt``  0
                          THEN  RepUR  ``new\_23\_sig\_vote\_with\_ballot\_first\_alt``  -1
                          )
              THEN  (BoolCase  \mkleeneopen{}new\_23\_sig\_vote\_with\_ballot(Cmd;notify;propose;f;es;x;n;0)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (DupHyp  (-1)
                          THEN  (RWO  "eqtt\_to\_assert<"  (-1)  THENA  Auto)
                          THEN  (HypSubst'  (-1)  (-3)  THEN  Reduce  (-3))
                          THEN  (FLemma  `new\_23\_sig\_vote\_with\_ballot-assert-type`  [-2]  THENA  Auto)\mcdot{})\mcdot{})\mcdot{})

---

Home Index