---

Step * of Lemma last-filter1

∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List].
  (last(filter(P;L)) = last(L) ∈ A) supposing ((↑(P last(L))) and (¬↑null(filter(P;L))))
BY
{ (Intros
   THEN Auto
   THEN (Assert ¬↑null(L) BY
               OnMaybeHyp 4 (\h. (ParallelOp h
                                  THEN (RW assert_pushdownC (-1) THENA Auto)
                                  THEN (HypSubst (-1) 0 THEN Complete (Auto)))))
   THEN Auto
   THEN PromoteHyp (-1) 4
   THEN ListInd 3
   THEN Reduce 0
   THEN Try (Complete (Auto))
   THEN AutoSplit
   THEN (RWO "last_cons2" 0 THENA Auto)
   THEN Repeat (AutoSplit)) }

1
1. A : Type
2. P : A ⟶ 𝔹
3. u : A
4. v : A List
5. ¬(filter(P;v) = [] ∈ (A List))
6. (¬↑null(v)) ⇒ (¬False) ⇒ (↑(P last(v))) ⇒ (last(filter(P;v)) = last(v) ∈ A)
7. ↑(P u)
8. v = [] ∈ (A List)
⊢ (¬False) ⇒ (¬False) ⇒ (↑(P u)) ⇒ (last(filter(P;v)) = u ∈ A)

2
1. A : Type
2. P : A ⟶ 𝔹
3. u : A
4. v : A List
5. ¬(v = [] ∈ (A List))
6. (¬False) ⇒ (¬↑null(filter(P;v))) ⇒ (↑(P last(v))) ⇒ (last(filter(P;v)) = last(v) ∈ A)
7. ↑(P u)
8. filter(P;v) = [] ∈ (A List)
⊢ (¬False) ⇒ (¬False) ⇒ (↑(P last(v))) ⇒ (u = last(v) ∈ A)

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  Auto
  THEN  (Assert  \mneg{}\muparrow{}null(L)  BY
                          OnMaybeHyp  4  (\mbackslash{}h.  (ParallelOp  h
                                                                THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
                                                                THEN  (HypSubst  (-1)  0  THEN  Complete  (Auto)))))
  THEN  Auto
  THEN  PromoteHyp  (-1)  4
  THEN  ListInd  3
  THEN  Reduce  0
  THEN  Try  (Complete  (Auto))
  THEN  AutoSplit
  THEN  (RWO  "last\_cons2"  0  THENA  Auto)
  THEN  Repeat  (AutoSplit))

---

Home Index