---

Step * 1 1 2 of Lemma listify_select_id


1. T : Type
2. n : ℕ
3. u : T
4. v : T List
5. ∀j:ℕ. (((j + ||v||) = n ∈ ℤ) ⇒ (listify(λi.v[i - j];j;n) = v ∈ (T List)))
6. j : ℕ
7. (j + ||v|| + 1) = n ∈ ℤ
⊢ listify(λi.[u / v][i - j];j;n) = [u / v] ∈ (T List)
BY
{ (RecCaseSplit `listify` THENA Auto{1,3}-1) }

1
.....truecase..... 
1. T : Type
2. n : ℕ
3. u : T
4. v : T List
5. ∀j:ℕ. (((j + ||v||) = n ∈ ℤ) ⇒ (listify(λi.v[i - j];j;n) = v ∈ (T List)))
6. j : ℕ
7. (j + ||v|| + 1) = n ∈ ℤ
8. n ≤ j
⊢ [] = [u / v] ∈ (T List)

2
1. T : Type
2. n : ℕ
3. u : T
4. v : T List
5. ∀j:ℕ. (((j + ||v||) = n ∈ ℤ) ⇒ (listify(λi.v[i - j];j;n) = v ∈ (T List)))
6. j : ℕ
7. (j + ||v|| + 1) = n ∈ ℤ
8. j < n
⊢ [[u / v][j - j] / listify(λi.[u / v][i - j];j + 1;n)] = [u / v] ∈ (T List)

---

Latex:

---

Latex:

1.  T  :  Type
2.  n  :  \mBbbN{}
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}j:\mBbbN{}.  (((j  +  ||v||)  =  n)  {}\mRightarrow{}  (listify(\mlambda{}i.v[i  -  j];j;n)  =  v))
6.  j  :  \mBbbN{}
7.  (j  +  ||v||  +  1)  =  n
\mvdash{}  listify(\mlambda{}i.[u  /  v][i  -  j];j;n)  =  [u  /  v]


By

---

Latex:
(RecCaseSplit  `listify`  THENA  Auto\{1,3\}-1)

---

Home Index