---

Step * 1 of Lemma swap_cons


1. T : Type
2. L : T List
3. x : T
4. i : ℕ+||L|| + 1
5. j : ℕ+||L|| + 1
6. i1 : ℕ
7. i1 < ||swap([x / L];i;j)||
⊢ swap([x / L];i;j)[i1] = [x / swap(L;i - 1;j - 1)][i1] ∈ T
BY
{ CaseNat 0 `i1' }

1
1. T : Type
2. L : T List
3. x : T
4. i : ℕ+||L|| + 1
5. j : ℕ+||L|| + 1
6. i1 : ℕ
7. i1 < ||swap([x / L];i;j)||
8. i1 = 0 ∈ ℤ
⊢ swap([x / L];i;j)[0] = [x / swap(L;i - 1;j - 1)][0] ∈ T

2
1. T : Type
2. L : T List
3. x : T
4. i : ℕ+||L|| + 1
5. j : ℕ+||L|| + 1
6. i1 : ℕ
7. i1 < ||swap([x / L];i;j)||
8. ¬(i1 = 0 ∈ ℤ)
⊢ swap([x / L];i;j)[i1] = [x / swap(L;i - 1;j - 1)][i1] ∈ T

---

Latex:

---

Latex:

1.  T  :  Type
2.  L  :  T  List
3.  x  :  T
4.  i  :  \mBbbN{}\msupplus{}||L||  +  1
5.  j  :  \mBbbN{}\msupplus{}||L||  +  1
6.  i1  :  \mBbbN{}
7.  i1  <  ||swap([x  /  L];i;j)||
\mvdash{}  swap([x  /  L];i;j)[i1]  =  [x  /  swap(L;i  -  1;j  -  1)][i1]


By

---

Latex:
CaseNat  0  `i1'

---

Home Index