---

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

∀Cmd:{T:Type| valueall-type(T)} . ∀propose,notify:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose).
∀es:EO+(Message(f)). ∀e:E. ∀n:ℤ. ∀e':E.
  (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
{ (UnivCD 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
⊢ 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'])

---

Latex:

---

Latex:
\mforall{}Cmd:\{T:Type|  valueall-type(T)\}  .  \mforall{}propose,notify:Atom  List.
\mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).  \mforall{}es:EO+(Message(f)).  \mforall{}e:E.  \mforall{}n:\mBbbZ{}.  \mforall{}e':E.
    (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:
(UnivCD  THENA  Auto)

---

Home Index