---

Step * of Lemma filter-length-less

No Annotations
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  ||filter(λx.P[x];L)|| < ||L|| supposing ∃x:T. ((x ∈ L) ∧ (¬↑P[x]))
BY
{ (InstLemma `filter-split-length` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN ExRepD
   THEN (Assert (x ∈ filter(λx.(¬bP[x]);L)) BY
               (GenListD 0 THEN Auto))
   THEN FLemma `l_member_length` [-1]
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    ||filter(\mlambda{}x.P[x];L)||  <  ||L||  supposing  \mexists{}x:T.  ((x  \mmember{}  L)  \mwedge{}  (\mneg{}\muparrow{}P[x]))


By

---

Latex:
(InstLemma  `filter-split-length`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD
  THEN  (Assert  (x  \mmember{}  filter(\mlambda{}x.(\mneg{}\msubb{}P[x]);L))  BY
                          (GenListD  0  THEN  Auto))
  THEN  FLemma  `l\_member\_length`  [-1]
  THEN  Auto)

---

Home Index