---

Step * 1 of Lemma last-mapfilter3


1. A : Type
2. B : Type
3. L : A List
4. ¬↑null(L)
5. P : A ⟶ 𝔹
6. f : {x:A| ↑(P x)}  ⟶ B
7. ¬↑null(mapfilter(f;P;L))
8. ↑(P last(L))
⊢ last(mapfilter(f;P;L)) = (f last(L)) ∈ B
BY
{ TACTIC:((RWO "last-mapfilter" 0 THENA Auto)
          THEN AutoSplit
          THEN Try (Complete ((D (-3)
                               THEN RepUR ``mapfilter`` 0
                               THEN (FLemma `equal-nil-sq-nil` [-1] THENA Auto)
                               THEN HypSubst (-1) 0
                               THEN Reduce 0
                               THEN Auto)))
          THEN EqCD
          THEN Auto) }

1
.....subterm..... T:t
2:n
1. A : Type
2. B : Type
3. L : A List
4. ¬↑null(L)
5. P : A ⟶ 𝔹
6. ¬(filter(P;L) = [] ∈ (A List))
7. f : {x:A| ↑(P x)}  ⟶ B
8. ¬↑null(mapfilter(f;P;L))
9. ↑(P last(L))
⊢ last(filter(P;L)) = last(L) ∈ {x:A| ↑(P x)} 

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  L  :  A  List
4.  \mneg{}\muparrow{}null(L)
5.  P  :  A  {}\mrightarrow{}  \mBbbB{}
6.  f  :  \{x:A|  \muparrow{}(P  x)\}    {}\mrightarrow{}  B
7.  \mneg{}\muparrow{}null(mapfilter(f;P;L))
8.  \muparrow{}(P  last(L))
\mvdash{}  last(mapfilter(f;P;L))  =  (f  last(L))


By

---

Latex:
TACTIC:((RWO  "last-mapfilter"  0  THENA  Auto)
                THEN  AutoSplit
                THEN  Try  (Complete  ((D  (-3)
                                                          THEN  RepUR  ``mapfilter``  0
                                                          THEN  (FLemma  `equal-nil-sq-nil`  [-1]  THENA  Auto)
                                                          THEN  HypSubst  (-1)  0
                                                          THEN  Reduce  0
                                                          THEN  Auto)))
                THEN  EqCD
                THEN  Auto)

---

Home Index