---

Step * 2 of Lemma length-filter-decreases


1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. (∃x∈v. ¬↑(P x)) ⇒ ||filter(P;v)|| < ||v||
6. ↑(P u)
7. (∃x∈[u / v]. ¬↑(P x))
⊢ ||filter(P;v)|| + 1 < ||v|| + 1
BY
{ (D (-3) THEN Auto) }

1
.....antecedent..... 
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ↑(P u)
6. (∃x∈[u / v]. ¬↑(P x))
⊢ (∃x∈v. ¬↑(P x))

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  u  :  T
4.  v  :  T  List
5.  (\mexists{}x\mmember{}v.  \mneg{}\muparrow{}(P  x))  {}\mRightarrow{}  ||filter(P;v)||  <  ||v||
6.  \muparrow{}(P  u)
7.  (\mexists{}x\mmember{}[u  /  v].  \mneg{}\muparrow{}(P  x))
\mvdash{}  ||filter(P;v)||  +  1  <  ||v||  +  1


By

---

Latex:
(D  (-3)  THEN  Auto)

---

Home Index