Step * 2 1 of Lemma nth_tl_decomp


1. Type
2. : ℤ
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 1 < ||L||
6. 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" 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