---

Step * 1 1 of Lemma select_listify_id


1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
⊢ ∀j:{...n}. ((0 ≤ j) ⇒ (∀i:{j..n-}. (listify(f;j;n)[i - j] = (f i) ∈ T)))
BY
{ ((BLemma `int_lower_ind` THENM UnivCD) THENA Auto') }

1
1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. 0 ≤ n
5. i : {n..n-}@i
⊢ listify(f;n;n)[i - n] = (f i) ∈ T

2
1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. j : {...n - 1}@i
5. (0 ≤ (j + 1)) ⇒ (∀i:{j + 1..n-}. (listify(f;j + 1;n)[i - j + 1] = (f i) ∈ T))
6. 0 ≤ j
7. i : {j..n-}@i
⊢ listify(f;j;n)[i - j] = (f i) ∈ T

3
1. T : Type
2. n : ℕ
3. f : ℕn ⟶ T
4. j : {...n - 1}@i
5. 0 ≤ (j + 1)
6. i : {j + 1..n-}@i
⊢ i - j + 1 < ||listify(f;j + 1;n)||

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  f  :  \mBbbN{}n  {}\mrightarrow{}  T
\mvdash{}  \mforall{}j:\{...n\}.  ((0  \mleq{}  j)  {}\mRightarrow{}  (\mforall{}i:\{j..n\msupminus{}\}.  (listify(f;j;n)[i  -  j]  =  (f  i))))


By

---

Latex:
((BLemma  `int\_lower\_ind`  THENM  UnivCD)  THENA  Auto')

---

Home Index