---

Step * of Lemma last-mapfilter2

∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[P:A ⟶ 𝔹]. ∀[L:A List].
  (last(mapfilter(f;P;L)) = (f last(L)) ∈ B) supposing ((↑(P last(L))) and (¬↑null(mapfilter(f;P;L))))
BY
{ (Intros
   THEN (Assert ¬↑null(L) BY
               (OnMaybeHyp 6 (\h. ParallelOp h)
                THEN (RW assert_pushdownC (-1) THENA Auto)
                THEN HypSubst (-1) 0
                THEN Auto))
   THEN Auto
   THEN PromoteHyp (-1) 6
   THEN (RWO "last-mapfilter" 0 THENA Auto)
   THEN AutoSplit
   THEN Try (Complete ((D (-3) THEN RepUR ``mapfilter`` 0 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. f : A ⟶ B
4. P : A ⟶ 𝔹
5. L : A List
6. ¬(filter(P;L) = [] ∈ (A List))
7. ¬↑null(L)
8. ¬↑null(mapfilter(f;P;L))
9. ↑(P last(L))
⊢ last(filter(P;L)) = last(L) ∈ A

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].
    (last(mapfilter(f;P;L))  =  (f  last(L)))  supposing  ((\muparrow{}(P  last(L)))  and  (\mneg{}\muparrow{}null(mapfilter(f;P;L))))


By

---

Latex:
(Intros
  THEN  (Assert  \mneg{}\muparrow{}null(L)  BY
                          (OnMaybeHyp  6  (\mbackslash{}h.  ParallelOp  h)
                            THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
                            THEN  HypSubst  (-1)  0
                            THEN  Auto))
  THEN  Auto
  THEN  PromoteHyp  (-1)  6
  THEN  (RWO  "last-mapfilter"  0  THENA  Auto)
  THEN  AutoSplit
  THEN  Try  (Complete  ((D  (-3)
                                            THEN  RepUR  ``mapfilter``  0
                                            THEN  HypSubst  (-1)  0
                                            THEN  Reduce  0
                                            THEN  Auto)))
  THEN  EqCD
  THEN  Auto)

---

Home Index