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` THEN Reduce 0)xxx }

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

2
1. Type
2. : ℤ
3. 0 < m
4. ∀[L:T List]. nth_tl(m 1;L) [L[m 1] nth_tl(1 (m 1);L)] supposing 1 < ||L||
⊢ ∀[L:T List]
    if m ≤then else nth_tl(m 1;tl(L)) fi  [L[m] if m ≤then 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