---

Step * 2 of Lemma lastn-cases

.....falsecase..... 
1. L : Top List
2. n : ℤ
3. n < ||L||
4. 0 < ||L|| - n
5. 0 < n
⊢ nth_tl(||L|| - n - 1;tl(L)) ~ lastn(n;tl(L))
BY
{ (Unfold `lastn` 0 THEN EqCD THEN Auto THEN DVar `L' THEN All Reduce THEN Auto')⋅ }

---

Latex:

---

Latex:
.....falsecase..... 
1.  L  :  Top  List
2.  n  :  \mBbbZ{}
3.  n  <  ||L||
4.  0  <  ||L||  -  n
5.  0  <  n
\mvdash{}  nth\_tl(||L||  -  n  -  1;tl(L))  \msim{}  lastn(n;tl(L))


By

---

Latex:
(Unfold  `lastn`  0  THEN  EqCD  THEN  Auto  THEN  DVar  `L'  THEN  All  Reduce  THEN  Auto')\mcdot{}

---

Home Index