---

Step * 2 1 of Lemma nth_tl_decomp


1. T : Type
2. m : ℤ
3. ¬(m ≤ 0)
4. 0 < m
5. ∀[L:T List]. nth_tl(m - 1;L) ~ [L[m - 1] / nth_tl(1 + (m - 1);L)] supposing m - 1 < ||L||
6. L : T List
7. m < ||L||
8. nth_tl(m - 1;tl(L)) ~ [tl(L)[m - 1] / nth_tl(1 + (m - 1);tl(L))]
⊢ tl(L)[m - 1] ~ L[m]
BY
{ (DVar `L' THEN All Reduce THEN Try (Complete (Auto)) THEN RWO "select-cons-tl" 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  m  :  \mBbbZ{}
3.  \mneg{}(m  \mleq{}  0)
4.  0  <  m
5.  \mforall{}[L:T  List].  nth\_tl(m  -  1;L)  \msim{}  [L[m  -  1]  /  nth\_tl(1  +  (m  -  1);L)]  supposing  m  -  1  <  ||L||
6.  L  :  T  List
7.  m  <  ||L||
8.  nth\_tl(m  -  1;tl(L))  \msim{}  [tl(L)[m  -  1]  /  nth\_tl(1  +  (m  -  1);tl(L))]
\mvdash{}  tl(L)[m  -  1]  \msim{}  L[m]


By

---

Latex:
(DVar  `L'  THEN  All  Reduce  THEN  Try  (Complete  (Auto))  THEN  RWO  "select-cons-tl"  0  THEN  Auto)\mcdot{}

---

Home Index