---

Step * 2 of Lemma nth_tl_decomp


1. T : Type
2. m : ℤ
3. 0 < m
4. ∀[L:T List]. nth_tl(m - 1;L) ~ [L[m - 1] / nth_tl(1 + (m - 1);L)] supposing m - 1 < ||L||
⊢ ∀[L:T List]
    if m ≤z 0 then L else nth_tl(m - 1;tl(L)) fi  ~ [L[m] / if 1 + m ≤z 0 then L else nth_tl((1 + m) - 1;tl(L)) fi ] 
    supposing m < ||L||
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN ((InstHyp [⌜tl(L)⌝] (-3) ⋅ THENM HypSubst' -1 0) THENA (RWW "length_tl" 0 THEN Auto))
   THEN AutoSplit
   THEN EqCD
   THEN Try (Complete (Auto))) }

1
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]

---

Latex:

---

Latex:

1.  T  :  Type
2.  m  :  \mBbbZ{}
3.  0  <  m
4.  \mforall{}[L:T  List].  nth\_tl(m  -  1;L)  \msim{}  [L[m  -  1]  /  nth\_tl(1  +  (m  -  1);L)]  supposing  m  -  1  <  ||L||
\mvdash{}  \mforall{}[L:T  List]
        if  m  \mleq{}z  0  then  L  else  nth\_tl(m  -  1;tl(L))  fi    \msim{}  [L[m]  / 
                                                                                                          if  1  +  m  \mleq{}z  0
                                                                                                          then  L
                                                                                                          else  nth\_tl((1  +  m)  -  1;tl(L))
                                                                                                          fi  ] 
        supposing  m  <  ||L||


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  ((InstHyp  [\mkleeneopen{}tl(L)\mkleeneclose{}]  (-3)  \mcdot{}  THENM  HypSubst'  -1  0)  THENA  (RWW  "length\_tl"  0  THEN  Auto))
  THEN  AutoSplit
  THEN  EqCD
  THEN  Try  (Complete  (Auto)))

---

Home Index