---

Step * 2 of Lemma last-filter1


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)
BY
{ ((RWO "assert_of_null<" (-1) THENA Auto)
   THEN (RWO "null-filter2" (-1) THENA Auto)
   THEN (Assert ⌜(last(v) ∈ v)⌝⋅ THENA Auto)
   THEN FLemma `l_all_fwd` [-2;-1]
   THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RWO  "assert\_of\_null<"  (-1)  THENA  Auto)
  THEN  (RWO  "null-filter2"  (-1)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}(last(v)  \mmember{}  v)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  FLemma  `l\_all\_fwd`  [-2;-1]
  THEN  Auto)

---

Home Index