---

Step * 1 of Lemma lastn-cases

.....truecase..... 
1. L : Top List
2. n : ℤ
3. n < ||L||
4. 0 < ||L|| - n
5. n ≤ 0
⊢ nth_tl(||L|| - n - 1;tl(L)) ~ []
BY
{ xxx(BLemma `nth_tl_is_nil` THEN Auto)xxx }

1
1. L : Top List
2. n : ℤ
3. n < ||L||
4. 0 < ||L|| - n
5. n ≤ 0
⊢ ||tl(L)|| ≤ (||L|| - n - 1)

---

Latex:

---

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


By

---

Latex:
xxx(BLemma  `nth\_tl\_is\_nil`  THEN  Auto)xxx

---

Home Index