---

Step * 2 of Lemma last-decomp2


1. l : Top List
2. ||l|| ≠ 0
⊢ l ~ firstn(||l|| - 1;l) @ [last(l)]
BY
{ (RWO "last-decomp<" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  l  :  Top  List
2.  ||l||  \mneq{}  0
\mvdash{}  l  \msim{}  firstn(||l||  -  1;l)  @  [last(l)]


By

---

Latex:
(RWO  "last-decomp<"  0  THEN  Auto)

---

Home Index