---

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


1. T : Type
2. u : T List
3. v : T List List
4. ((¬↑null(concat(v))) ∧ (last(concat(v)) = last(last(v)) ∈ T)) supposing ((¬↑null(last(v))) and (¬↑null(v)))
⊢ ((¬↑null(concat([u / v]))) ∧ (last(concat([u / v])) = last(last([u / v])) ∈ T)) supposing 
     ((¬↑null(last([u / v]))) and 
     (¬False))
BY
{ DVar `v' }

1
1. T : Type
2. u : T List
3. ((¬↑null(concat([]))) ∧ (last(concat([])) = last(last([])) ∈ T)) supposing ((¬↑null(last([]))) and (¬↑null([])))
⊢ ((¬↑null(concat([u]))) ∧ (last(concat([u])) = last(last([u])) ∈ T)) supposing ((¬↑null(last([u]))) and (¬False))

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

---

Latex:

---

Latex:

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


By

---

Latex:
DVar  `v'

---

Home Index