---

Step * of Lemma select-remove-first

∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹]. ∀[i:ℕ||remove-first(P;L)||].
  (remove-first(P;L)[i] ~ L[i] supposing ∀j:ℕi + 1. (¬↑(P L[j]))
  ∧ remove-first(P;L)[i] ~ L[i + 1] supposing ∃j:ℕi + 1. (↑(P L[j])))
BY
{ TACTIC:(RepeatFor 3 ((D 0
                        THENA (Auto
                               THEN (Assert ||remove-first(P;L)|| ≤ ||L|| BY
                                           BLemma `length-remove-first-le`)
                               THEN Auto)
                        ))
          THEN ((Assert ||remove-first(P;L)|| ≤ ||L|| BY
                       (BLemma `length-remove-first-le` THEN Auto))
                THEN (D 0 THENA Auto)
                THEN ListInd 2
                THEN Unfold `remove-first` 0
                THEN Reduce 0
                THEN Try (Fold `remove-first` 0)
                THEN (D 0 THENA Auto)
                THEN Try (Complete (Auto))
                THEN (Assert P u ∈ 𝔹 BY
                            Auto)
                THEN (Assert P ∈ {x:T| (x ∈ v)}  ⟶ 𝔹 BY
                            ExtWith [`z'] [{x:T| (x ∈ [u / v])}  ⟶ 𝔹] ⋅
                            THEN Auto)
                THEN (InstHyp [⌜P⌝] (-4)⋅ THENA (Auto THEN BLemma `length-remove-first-le` THEN Auto))
                THEN Thin (-5)
                THEN (AutoSplit THENA 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)
⊢ (||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]))))

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])))
⊢ ((||remove-first(P;v)|| + 1) ≤ (||v|| + 1))
⇒ (∀i:ℕ||remove-first(P;v)|| + 1
      ([u / remove-first(P;v)][i] ~ [u / v][i] supposing ∀j:ℕi + 1. (¬↑(P [u / v][j]))
      ∧ [u / remove-first(P;v)][i] ~ [u / v][i + 1] supposing ∃j:ℕi + 1. (↑(P [u / v][j]))))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].  \mforall{}[i:\mBbbN{}||remove-first(P;L)||].
    (remove-first(P;L)[i]  \msim{}  L[i]  supposing  \mforall{}j:\mBbbN{}i  +  1.  (\mneg{}\muparrow{}(P  L[j]))
    \mwedge{}  remove-first(P;L)[i]  \msim{}  L[i  +  1]  supposing  \mexists{}j:\mBbbN{}i  +  1.  (\muparrow{}(P  L[j])))


By

---

Latex:
TACTIC:(RepeatFor  3  ((D  0
                                            THENA  (Auto
                                                          THEN  (Assert  ||remove-first(P;L)||  \mleq{}  ||L||  BY
                                                                                  BLemma  `length-remove-first-le`)
                                                          THEN  Auto)
                                            ))
                THEN  ((Assert  ||remove-first(P;L)||  \mleq{}  ||L||  BY
                                          (BLemma  `length-remove-first-le`  THEN  Auto))
                            THEN  (D  0  THENA  Auto)
                            THEN  ListInd  2
                            THEN  Unfold  `remove-first`  0
                            THEN  Reduce  0
                            THEN  Try  (Fold  `remove-first`  0)
                            THEN  (D  0  THENA  Auto)
                            THEN  Try  (Complete  (Auto))
                            THEN  (Assert  P  u  \mmember{}  \mBbbB{}  BY
                                                    Auto)
                            THEN  (Assert  P  \mmember{}  \{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  \mBbbB{}  BY
                                                    ExtWith  [`z']  [\{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  \mBbbB{}]  \mcdot{}
                                                    THEN  Auto)
                            THEN  (InstHyp  [\mkleeneopen{}P\mkleeneclose{}]  (-4)\mcdot{}  THENA  (Auto  THEN  BLemma  `length-remove-first-le`  THEN  Auto))
                            THEN  Thin  (-5)
                            THEN  (AutoSplit  THENA  Auto)\mcdot{})\mcdot{}
                )

---

Home Index