---

Step * of Lemma rcvd-innings-nil

∀[V:Type]. ∀[A:Id List]. ∀[L:consensus-rcv(V;A) List]. ∀[i,n:ℤ].
  (filter(λr.i <z inning(r);L) ~ []) supposing 
     ((n ≤ i) and 
     (filter(λr.n <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List)))
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "filter_is_nil" 0 THENM Reduce 0)
   THEN Auto
   THEN RepUR ``so_apply`` 0
   THEN BLemma `l_all_iff`
   THEN Auto
   THEN D 0
   THEN Auto) }

1
1. V : Type
2. A : Id List
3. L : consensus-rcv(V;A) List
4. i : ℤ
5. n : ℤ
6. filter(λr.n <z inning(r);L) = [] ∈ (consensus-rcv(V;A) List)
7. n ≤ i
8. x : consensus-rcv(V;A)@i
9. (x ∈ L)@i
10. ↑i <z inning(x)@i
⊢ False

---

Latex:


\mforall{}[V:Type].  \mforall{}[A:Id  List].  \mforall{}[L:consensus-rcv(V;A)  List].  \mforall{}[i,n:\mBbbZ{}].
    (filter(\mlambda{}r.i  <z  inning(r);L)  \msim{}  [])  supposing  ((n  \mleq{}  i)  and  (filter(\mlambda{}r.n  <z  inning(r);L)  =  []))


By

((UnivCD  THENA  Auto)
  THEN  (RWO  "filter\_is\_nil"  0  THENM  Reduce  0)
  THEN  Auto
  THEN  RepUR  ``so\_apply``  0
  THEN  BLemma  `l\_all\_iff`
  THEN  Auto
  THEN  D  0
  THEN  Auto)

---

Home Index