---

Step * of Lemma last-mapfilter3

No Annotations
∀[A,B:Type]. ∀[L:A List]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑(P x)}  ⟶ B].
  (last(mapfilter(f;P;L)) = (f last(L)) ∈ B) supposing ((↑(P last(L))) and (¬↑null(mapfilter(f;P;L))))
BY
{ TACTIC:TACTIC:(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) 4) }

1
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

---

Latex:

---

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


By

---

Latex:
TACTIC:TACTIC:(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)  4)

---

Home Index