---

Step * 2 2 1 1 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([u1 / v]))
7. (¬↑null(concat([u1 / v]))) ∧ (last(concat([u1 / v])) = last(last([u1 / v])) ∈ T)
⊢ (¬↑null(u @ concat([u1 / v]))) ∧ (last(u @ concat([u1 / v])) = last(last([u; [u1 / v]])) ∈ T)
BY
{ 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]))
8. last(concat([u1 / v])) = last(last([u1 / v])) ∈ T
⊢ ¬↑null(u @ concat([u1 / v]))

2
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]))
8. last(concat([u1 / v])) = last(last([u1 / v])) ∈ T
9. ¬↑null(u @ concat([u1 / v]))
⊢ last(u @ concat([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([u1  /  v]))
7.  (\mneg{}\muparrow{}null(concat([u1  /  v])))  \mwedge{}  (last(concat([u1  /  v]))  =  last(last([u1  /  v])))
\mvdash{}  (\mneg{}\muparrow{}null(u  @  concat([u1  /  v])))  \mwedge{}  (last(u  @  concat([u1  /  v]))  =  last(last([u;  [u1  /  v]])))


By

---

Latex:
Auto

---

Home Index