---

Step * 2 1 1 of Lemma select-firstn


1. u : Top
2. v : Top List
3. ∀m:ℕ||v||. ∀x:ℕm.  (firstn(m;v)[x] ~ v[x])
4. m : ℕ||v|| + 1
5. x : ℕm
6. 0 < m
7. ¬(x = 0 ∈ ℤ)
⊢ [u / firstn(m - 1;v)][x] ~ [u / v][x]
BY
{ Subst' x ~ (x - 1) + 1 0 }

1
.....equality..... 
1. u : Top
2. v : Top List
3. ∀m:ℕ||v||. ∀x:ℕm.  (firstn(m;v)[x] ~ v[x])
4. m : ℕ||v|| + 1
5. x : ℕm
6. 0 < m
7. ¬(x = 0 ∈ ℤ)
⊢ x ~ (x - 1) + 1

2
1. u : Top
2. v : Top List
3. ∀m:ℕ||v||. ∀x:ℕm.  (firstn(m;v)[x] ~ v[x])
4. m : ℕ||v|| + 1
5. x : ℕm
6. 0 < m
7. ¬(x = 0 ∈ ℤ)
⊢ [u / firstn(m - 1;v)][(x - 1) + 1] ~ [u / v][(x - 1) + 1]

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}m:\mBbbN{}||v||.  \mforall{}x:\mBbbN{}m.    (firstn(m;v)[x]  \msim{}  v[x])
4.  m  :  \mBbbN{}||v||  +  1
5.  x  :  \mBbbN{}m
6.  0  <  m
7.  \mneg{}(x  =  0)
\mvdash{}  [u  /  firstn(m  -  1;v)][x]  \msim{}  [u  /  v][x]


By

---

Latex:
Subst'  x  \msim{}  (x  -  1)  +  1  0

---

Home Index