---

Step * 3 of Lemma length-filter-decreases


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

---

Latex:

---

Latex:

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


By

---

Latex:
(InstLemma  `length-filter`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THEN  Auto')\mcdot{}

---

Home Index