---

Step * 2 2 1 of Lemma last-concat-non-null


1. T : Type
2. u : T List
3. u1 : T List
4. v : T List List
5. ¬False
6. ¬↑null(last([u; [u1 / v]]))
7. (¬↑null(concat([u1 / v]))) ∧ (last(concat([u1 / v])) = last(last([u1 / v])) ∈ T)
⊢ (¬↑null(concat([u; [u1 / v]]))) ∧ (last(concat([u; [u1 / v]])) = last(last([u; [u1 / v]])) ∈ T)
BY
{ (RWO "last_cons" (-2) THENA Auto)⋅ }

1
1. T : Type
2. u : T List
3. u1 : T List
4. v : T List List
5. ¬False
6. ¬↑null(last([u1 / v]))
7. (¬↑null(concat([u1 / v]))) ∧ (last(concat([u1 / v])) = last(last([u1 / v])) ∈ T)
⊢ (¬↑null(concat([u; [u1 / v]]))) ∧ (last(concat([u; [u1 / v]])) = last(last([u; [u1 / v]])) ∈ T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T  List
3.  u1  :  T  List
4.  v  :  T  List  List
5.  \mneg{}False
6.  \mneg{}\muparrow{}null(last([u;  [u1  /  v]]))
7.  (\mneg{}\muparrow{}null(concat([u1  /  v])))  \mwedge{}  (last(concat([u1  /  v]))  =  last(last([u1  /  v])))
\mvdash{}  (\mneg{}\muparrow{}null(concat([u;  [u1  /  v]])))  \mwedge{}  (last(concat([u;  [u1  /  v]]))  =  last(last([u;  [u1  /  v]])))


By

---

Latex:
(RWO  "last\_cons"  (-2)  THENA  Auto)\mcdot{}

---

Home Index