---

Step * of Lemma length-list-delete

∀[T:Type]. ∀[as:T List]. ∀[i:ℕ].  ||as\i|| = (||as|| - 1) ∈ ℤ supposing i < ||as||
BY
{ (InductionOnList THEN (UnivCD THENA Auto) THEN RecUnfold `list-delete` 0 THEN Reduce 0 THEN Auto) }

1
1. T : Type
2. i : ℕ
3. i < ||[]||
⊢ 0 = (-1) ∈ ℤ

2
1. T : Type
2. u : T
3. v : T List
4. ∀[i:ℕ]. ||v\i|| = (||v|| - 1) ∈ ℤ supposing i < ||v||
5. i : ℕ
6. i < ||[u / v]||
⊢ ||if (i) < (1)  then v  else [u / v\i - 1]|| = ((||v|| + 1) - 1) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[as:T  List].  \mforall{}[i:\mBbbN{}].    ||as\mbackslash{}i||  =  (||as||  -  1)  supposing  i  <  ||as||


By

---

Latex:
(InductionOnList  THEN  (UnivCD  THENA  Auto)  THEN  RecUnfold  `list-delete`  0  THEN  Reduce  0  THEN  Auto)

---

Home Index