---

Step * of Lemma last-decomp

No Annotations
∀[l:Top List]. l ~ firstn(||l|| - 1;l) @ [last(l)] supposing 0 < ||l||
BY
{ (Auto
   THEN InstLemma `firstn_decomp2` [⌜Top⌝;⌜||l||⌝;⌜l⌝]⋅
   THEN Auto
   THEN Fold `last` (-1)
   THEN RWO "-1" 0
   THEN RWO "firstn_all" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[l:Top  List].  l  \msim{}  firstn(||l||  -  1;l)  @  [last(l)]  supposing  0  <  ||l||


By

---

Latex:
(Auto
  THEN  InstLemma  `firstn\_decomp2`  [\mkleeneopen{}Top\mkleeneclose{};\mkleeneopen{}||l||\mkleeneclose{};\mkleeneopen{}l\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Fold  `last`  (-1)
  THEN  RWO  "-1"  0
  THEN  RWO  "firstn\_all"  0
  THEN  Auto)

---

Home Index