---

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


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))
BY
{ ((RepUR ``concat last`` 0 THEN Fold `last` 0) THEN RWO "append-nil" 0 THEN Auto) }

---

Latex:

---

Latex:

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


By

---

Latex:
((RepUR  ``concat  last``  0  THEN  Fold  `last`  0)  THEN  RWO  "append-nil"  0  THEN  Auto)

---

Home Index