---

Step * of Lemma nth_tl_decomp

∀[T:Type]. ∀[m:ℕ]. ∀[L:T List].  nth_tl(m;L) ~ [L[m] / nth_tl(1 + m;L)] supposing m < ||L||
BY
{ xxx(InductionOnNat THEN RecUnfold `nth_tl` 0 THEN Reduce 0)xxx }

1
1. T : Type
2. m : ℤ
⊢ ∀[L:T List]. L ~ [L[0] / tl(L)] supposing 0 < ||L||

2
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||

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[L:T  List].    nth\_tl(m;L)  \msim{}  [L[m]  /  nth\_tl(1  +  m;L)]  supposing  m  <  ||L||


By

---

Latex:
xxx(InductionOnNat  THEN  RecUnfold  `nth\_tl`  0  THEN  Reduce  0)xxx

---

Home Index