---

Step * 1 1 of Lemma last-mapfilter3

.....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)} 
BY
{ TACTIC:(ListInd 3
          THEN Reduce 0
          THEN Try (Complete (Auto))
          THEN ((Unfold `mapfilter` -1 THEN (RWO "null-map" (-1) THENA Auto))
                THEN Unfold `mapfilter` 0
                THEN (RWO "null-map" 0 THENA Auto))
          THEN Reduce 0
          THEN AutoSplit
          THEN (RWO "last-cons" 0 THENA Auto)
          THEN AutoSplit) }

1
1. A : Type
2. B : Type
3. P : A ⟶ 𝔹
4. f : {x:A| ↑(P x)}  ⟶ B
5. u : A@i
6. v : A List@i
7. (¬↑null(v))
⇒ (¬(filter(P;v) = [] ∈ (A List)))
⇒ (¬↑null(filter(P;v)))
⇒ (↑(P last(v)))
⇒ (last(filter(P;v)) = last(v) ∈ {x:A| ↑(P x)} )
8. ↑(P u)
9. v = [] ∈ (A List)
⊢ (¬False)
⇒ (¬([u / filter(P;v)] = [] ∈ (A List)))
⇒ (¬False)
⇒ (↑(P u))
⇒ (if null(filter(P;v)) then u else last(filter(P;v)) fi  = u ∈ {x:A| ↑(P x)} )

2
1. A : Type
2. B : Type
3. P : A ⟶ 𝔹
4. f : {x:A| ↑(P x)}  ⟶ B
5. u : A@i
6. v : A List@i
7. ¬(v = [] ∈ (A List))
8. (¬False)
⇒ (¬(filter(P;v) = [] ∈ (A List)))
⇒ (¬↑null(filter(P;v)))
⇒ (↑(P last(v)))
⇒ (last(filter(P;v)) = last(v) ∈ {x:A| ↑(P x)} )
9. ↑(P u)
⊢ (¬False)
⇒ (¬([u / filter(P;v)] = [] ∈ (A List)))
⇒ (¬False)
⇒ (↑(P last(v)))
⇒ (if null(filter(P;v)) then u else last(filter(P;v)) fi  = last(v) ∈ {x:A| ↑(P x)} )

---

Latex:

---

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


By

---

Latex:
TACTIC:(ListInd  3
                THEN  Reduce  0
                THEN  Try  (Complete  (Auto))
                THEN  ((Unfold  `mapfilter`  -1  THEN  (RWO  "null-map"  (-1)  THENA  Auto))
                            THEN  Unfold  `mapfilter`  0
                            THEN  (RWO  "null-map"  0  THENA  Auto))
                THEN  Reduce  0
                THEN  AutoSplit
                THEN  (RWO  "last-cons"  0  THENA  Auto)
                THEN  AutoSplit)

---

Home Index