---

Step * 1 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. P ∈ {x:T| (x ∈ v)}  ⟶ 𝔹
7. ∀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])))
8. ↑(P u)
⊢ (||v|| ≤ (||v|| + 1))
⇒ (∀i:ℕ||v||
      (v[i] ~ [u / v][i] supposing ∀j:ℕi + 1. (¬↑(P [u / v][j]))
      ∧ v[i] ~ [u / v][i + 1] supposing ∃j:ℕi + 1. (↑(P [u / v][j]))))
BY
{ ((D 0 THENA Auto) THEN Thin (-1) THEN RepeatFor 3 ((D 0 THENA Thin 6 THEN Auto))) }

1
1. T : Type
2. u : T
3. v : T List
4. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
5. P u ∈ 𝔹
6. P ∈ {x:T| (x ∈ v)}  ⟶ 𝔹
7. ∀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])))
8. ↑(P u)
9. i : ℕ||v||
10. ∀j:ℕi + 1. (¬↑(P [u / v][j]))
⊢ v[i] ~ [u / v][i]

2
1. T : Type
2. u : T
3. v : T List
4. P : {x:T| (x ∈ [u / v])}  ⟶ 𝔹
5. P u ∈ 𝔹
6. P ∈ {x:T| (x ∈ v)}  ⟶ 𝔹
7. ∀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])))
8. ↑(P u)
9. i : ℕ||v||
10. ∃j:ℕi + 1. (↑(P [u / v][j]))
⊢ 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.  P  u  \mmember{}  \mBbbB{}
6.  P  \mmember{}  \{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  \mBbbB{}
7.  \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])))
8.  \muparrow{}(P  u)
\mvdash{}  (||v||  \mleq{}  (||v||  +  1))
{}\mRightarrow{}  (\mforall{}i:\mBbbN{}||v||
            (v[i]  \msim{}  [u  /  v][i]  supposing  \mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(P  [u  /  v][j]))
            \mwedge{}  v[i]  \msim{}  [u  /  v][i  +  1]  supposing  \mexists{}j:\mBbbN{}i  +  1.  (\muparrow{}(P  [u  /  v][j]))))


By

---

Latex:
((D  0  THENA  Auto)  THEN  Thin  (-1)  THEN  RepeatFor  3  ((D  0  THENA  Thin  6  THEN  Auto)))

---

Home Index