---

Step * 1 1 of Lemma last-mapfilter2


1. A : Type
2. B : Type
3. f : A ⟶ B
4. P : A ⟶ 𝔹
5. u : A
6. v : A List
7. ¬(filter(P;v) = [] ∈ (A List))
8. ↑(P u)
9. v = [] ∈ (A List)
10. ¬([u / filter(P;v)] = [] ∈ (A List))
11. ¬False
12. ¬↑null(mapfilter(f;P;[u / v]))
13. ↑(P u)
14. (¬↑null(v)) ⇒ (¬↑null(mapfilter(f;P;v))) ⇒ (↑(P last(v))) ⇒ (last(filter(P;v)) = last(v) ∈ A)
⊢ last(filter(P;v)) = u ∈ A
BY
{ (D 7 THEN Eliminate ⌜v⌝⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  P  :  A  {}\mrightarrow{}  \mBbbB{}
5.  u  :  A
6.  v  :  A  List
7.  \mneg{}(filter(P;v)  =  [])
8.  \muparrow{}(P  u)
9.  v  =  []
10.  \mneg{}([u  /  filter(P;v)]  =  [])
11.  \mneg{}False
12.  \mneg{}\muparrow{}null(mapfilter(f;P;[u  /  v]))
13.  \muparrow{}(P  u)
14.  (\mneg{}\muparrow{}null(v))  {}\mRightarrow{}  (\mneg{}\muparrow{}null(mapfilter(f;P;v)))  {}\mRightarrow{}  (\muparrow{}(P  last(v)))  {}\mRightarrow{}  (last(filter(P;v))  =  last(v))
\mvdash{}  last(filter(P;v))  =  u


By

---

Latex:
(D  7  THEN  Eliminate  \mkleeneopen{}v\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index