---

Step * 1 of Lemma last-mapfilter2

.....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
BY
{ (ListInd (-5)
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN AutoSplit
   THEN (RWO "last-cons" 0 THENA Auto)
   THEN Repeat (AutoSplit)
   THEN Auto
   THEN Try (Complete ((BackThruSomeHyp
                        THEN Auto
                        THEN RepUR ``mapfilter`` 0
                        THEN (RWO "null-map" 0 THENA Auto)
                        THEN RW assert_pushdownC 0
                        THEN Auto)))) }

1
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

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

---

Latex:

---

Latex:
.....subterm.....  T:t
2:n
1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  B
4.  P  :  A  {}\mrightarrow{}  \mBbbB{}
5.  L  :  A  List
6.  \mneg{}(filter(P;L)  =  [])
7.  \mneg{}\muparrow{}null(L)
8.  \mneg{}\muparrow{}null(mapfilter(f;P;L))
9.  \muparrow{}(P  last(L))
\mvdash{}  last(filter(P;L))  =  last(L)


By

---

Latex:
(ListInd  (-5)
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  AutoSplit
  THEN  (RWO  "last-cons"  0  THENA  Auto)
  THEN  Repeat  (AutoSplit)
  THEN  Auto
  THEN  Try  (Complete  ((BackThruSomeHyp
                                            THEN  Auto
                                            THEN  RepUR  ``mapfilter``  0
                                            THEN  (RWO  "null-map"  0  THENA  Auto)
                                            THEN  RW  assert\_pushdownC  0
                                            THEN  Auto))))

---

Home Index