---

Step * 1 of Lemma last-filter1


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)
BY
{ ((HypSubst (-1) (-4) THENA Auto) THEN D (-4) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbB{}
3.  u  :  A
4.  v  :  A  List
5.  \mneg{}(filter(P;v)  =  [])
6.  (\mneg{}\muparrow{}null(v))  {}\mRightarrow{}  (\mneg{}False)  {}\mRightarrow{}  (\muparrow{}(P  last(v)))  {}\mRightarrow{}  (last(filter(P;v))  =  last(v))
7.  \muparrow{}(P  u)
8.  v  =  []
\mvdash{}  (\mneg{}False)  {}\mRightarrow{}  (\mneg{}False)  {}\mRightarrow{}  (\muparrow{}(P  u))  {}\mRightarrow{}  (last(filter(P;v))  =  u)


By

---

Latex:
((HypSubst  (-1)  (-4)  THENA  Auto)  THEN  D  (-4)  THEN  Reduce  0  THEN  Auto)

---

Home Index