---

Step * 2 2 1 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]))
8. last(concat([u1 / v])) = last(last([u1 / v])) ∈ T
⊢ ¬↑null(u @ concat([u1 / v]))
BY
{ (ParallelOp -2
   THEN RWO "null_append" (-1)
   THEN Auto
   THEN ((RW assert_pushdownC (-1) THENM RW assert_pushdownC 0) THEN Auto)⋅) }

---

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]))
8.  last(concat([u1  /  v]))  =  last(last([u1  /  v]))
\mvdash{}  \mneg{}\muparrow{}null(u  @  concat([u1  /  v]))


By

---

Latex:
(ParallelOp  -2
  THEN  RWO  "null\_append"  (-1)
  THEN  Auto
  THEN  ((RW  assert\_pushdownC  (-1)  THENM  RW  assert\_pushdownC  0)  THEN  Auto)\mcdot{})

---

Home Index