---

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


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))
BY
{ ((ParallelLast THENA (Reduce 0 THEN Auto)) THEN (ParallelLast THENA (RWO "last_cons" (-1) THEN Auto))) }

1
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)

---

Latex:

---

Latex:

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


By

---

Latex:
((ParallelLast  THENA  (Reduce  0  THEN  Auto))
  THEN  (ParallelLast  THENA  (RWO  "last\_cons"  (-1)  THEN  Auto))
  )

---

Home Index