---

Step * 1 of Lemma mapfilter-pos-length


1. T : Type
2. B : Type
3. L : T List
4. P : {x:T| (x ∈ L)}  ⟶ 𝔹
5. f : {x:{x:T| (x ∈ L)} | ↑(P x)}  ⟶ B
⊢ (¬(mapfilter(f;P;L) = [] ∈ (B List))) ⇒ 0 < ||mapfilter(f;P;L)||
BY
{ ((GenConclAtAddr [2;2;1] THENA Auto) THEN D -2 THEN Reduce 0 THEN Auto' THEN D -1 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  B  :  Type
3.  L  :  T  List
4.  P  :  \{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}
5.  f  :  \{x:\{x:T|  (x  \mmember{}  L)\}  |  \muparrow{}(P  x)\}    {}\mrightarrow{}  B
\mvdash{}  (\mneg{}(mapfilter(f;P;L)  =  []))  {}\mRightarrow{}  0  <  ||mapfilter(f;P;L)||


By

---

Latex:
((GenConclAtAddr  [2;2;1]  THENA  Auto)  THEN  D  -2  THEN  Reduce  0  THEN  Auto'  THEN  D  -1  THEN  Auto)\mcdot{}

---

Home Index