---

Step * of Lemma general_length_nth_tl

∀[r:ℕ]. ∀[L:Top List].  (||nth_tl(r;L)|| = if r <z ||L|| then ||L|| - r else 0 fi  ∈ ℤ)
BY
{ xxx(InductionOnNat THEN RecUnfold `nth_tl` 0 THEN Reduce 0)xxx }

1
1. r : ℤ
⊢ ∀[L:Top List]. (||L|| = if 0 <z ||L|| then ||L|| - 0 else 0 fi  ∈ ℤ)

2
1. r : ℤ
2. 0 < r
3. ∀[L:Top List]. (||nth_tl(r - 1;L)|| = if r - 1 <z ||L|| then ||L|| - r - 1 else 0 fi  ∈ ℤ)
⊢ ∀[L:Top List]. (||if r ≤z 0 then L else nth_tl(r - 1;tl(L)) fi || = if r <z ||L|| then ||L|| - r else 0 fi  ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}[r:\mBbbN{}].  \mforall{}[L:Top  List].    (||nth\_tl(r;L)||  =  if  r  <z  ||L||  then  ||L||  -  r  else  0  fi  )


By

---

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

---

Home Index