---

Step * 2 2 2 1 2 2 of Lemma select-remove-first


1. T : Type
2. u : T
3. v : T List
4. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
5. ¬↑(P u)
6. ff ∈ 𝔹
7. P ∈ {x:T| (x ∈ v)}  ⟶ 𝔹
8. ∀i:ℕ||remove-first(P;v)||
     (remove-first(P;v)[i] ~ v[i] supposing ∀j:ℕi + 1. (¬↑(P v[j]))
     ∧ remove-first(P;v)[i] ~ v[i + 1] supposing ∃j:ℕi + 1. (↑(P v[j])))
9. i : ℕ||remove-first(P;v)|| + 1
10. ¬(i = 0 ∈ ℤ)
11. remove-first(P;v)[i - 1] ~ v[i - 1] supposing ∀j:ℕ(i - 1) + 1. (¬↑(P v[j]))
12. remove-first(P;v)[i - 1] ~ v[(i - 1) + 1] supposing ∃j:ℕ(i - 1) + 1. (↑(P v[j]))
13. j : ℕi + 1
14. ↑(P [u / v][j])
15. ¬(j = 0 ∈ ℤ)
16. (∃x∈v. ↑(P x))
17. ||remove-first(P;v)|| = (||v|| - 1) ∈ ℤ
⊢ [u / remove-first(P;v)][i] ~ [u / v][i + 1]
BY
{ D (-6) }

1
.....antecedent..... 
1. T : Type
2. u : T
3. v : T List
4. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
5. ¬↑(P u)
6. ff ∈ 𝔹
7. P ∈ {x:T| (x ∈ v)}  ⟶ 𝔹
8. ∀i:ℕ||remove-first(P;v)||
     (remove-first(P;v)[i] ~ v[i] supposing ∀j:ℕi + 1. (¬↑(P v[j]))
     ∧ remove-first(P;v)[i] ~ v[i + 1] supposing ∃j:ℕi + 1. (↑(P v[j])))
9. i : ℕ||remove-first(P;v)|| + 1
10. ¬(i = 0 ∈ ℤ)
11. remove-first(P;v)[i - 1] ~ v[i - 1] supposing ∀j:ℕ(i - 1) + 1. (¬↑(P v[j]))
12. j : ℕi + 1
13. ↑(P [u / v][j])
14. ¬(j = 0 ∈ ℤ)
15. (∃x∈v. ↑(P x))
16. ||remove-first(P;v)|| = (||v|| - 1) ∈ ℤ
⊢ ∃j:ℕ(i - 1) + 1. (↑(P v[j]))

2
1. T : Type
2. u : T
3. v : T List
4. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
5. ¬↑(P u)
6. ff ∈ 𝔹
7. P ∈ {x:T| (x ∈ v)}  ⟶ 𝔹
8. ∀i:ℕ||remove-first(P;v)||
     (remove-first(P;v)[i] ~ v[i] supposing ∀j:ℕi + 1. (¬↑(P v[j]))
     ∧ remove-first(P;v)[i] ~ v[i + 1] supposing ∃j:ℕi + 1. (↑(P v[j])))
9. i : ℕ||remove-first(P;v)|| + 1
10. ¬(i = 0 ∈ ℤ)
11. remove-first(P;v)[i - 1] ~ v[i - 1] supposing ∀j:ℕ(i - 1) + 1. (¬↑(P v[j]))
12. j : ℕi + 1
13. ↑(P [u / v][j])
14. ¬(j = 0 ∈ ℤ)
15. (∃x∈v. ↑(P x))
16. ||remove-first(P;v)|| = (||v|| - 1) ∈ ℤ
17. remove-first(P;v)[i - 1] ~ v[(i - 1) + 1]
⊢ [u / remove-first(P;v)][i] ~ [u / v][i + 1]

---

Latex:

---

Latex:

1.  T  :  Type
2.  u  :  T
3.  v  :  T  List
4.  P  :  \{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  \mBbbB{}
5.  \mneg{}\muparrow{}(P  u)
6.  ff  \mmember{}  \mBbbB{}
7.  P  \mmember{}  \{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  \mBbbB{}
8.  \mforall{}i:\mBbbN{}||remove-first(P;v)||
          (remove-first(P;v)[i]  \msim{}  v[i]  supposing  \mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(P  v[j]))
          \mwedge{}  remove-first(P;v)[i]  \msim{}  v[i  +  1]  supposing  \mexists{}j:\mBbbN{}i  +  1.  (\muparrow{}(P  v[j])))
9.  i  :  \mBbbN{}||remove-first(P;v)||  +  1
10.  \mneg{}(i  =  0)
11.  remove-first(P;v)[i  -  1]  \msim{}  v[i  -  1]  supposing  \mforall{}j:\mBbbN{}(i  -  1)  +  1.  (\mneg{}\muparrow{}(P  v[j]))
12.  remove-first(P;v)[i  -  1]  \msim{}  v[(i  -  1)  +  1]  supposing  \mexists{}j:\mBbbN{}(i  -  1)  +  1.  (\muparrow{}(P  v[j]))
13.  j  :  \mBbbN{}i  +  1
14.  \muparrow{}(P  [u  /  v][j])
15.  \mneg{}(j  =  0)
16.  (\mexists{}x\mmember{}v.  \muparrow{}(P  x))
17.  ||remove-first(P;v)||  =  (||v||  -  1)
\mvdash{}  [u  /  remove-first(P;v)][i]  \msim{}  [u  /  v][i  +  1]


By

---

Latex:
D  (-6)

---

Home Index