---

Step * 2 of Lemma equipollent-filter


1. [A] : Type
2. P : A ⟶ 𝔹
⊢ ∀ys:A List. ∀y:A.
    ({x:ℕ||ys||| ↑P[ys[x]]}  ~ ℕ||filter(P;ys)|| ⇒ {x:ℕ||ys @ [y]||| ↑P[ys @ [y][x]]}  ~ ℕ||filter(P;ys @ [y])||)
BY
{ (Auto
   THEN (RWO "filter_append" 0 THENA Auto)
   THEN (RWO "length-append" 0 THENA Auto)
   THEN Reduce 0
   THEN SplitOnConclITE
   THEN Auto
   THEN Reduce 0) }

1
1. [A] : Type
2. P : A ⟶ 𝔹
3. ys : A List
4. y : A
5. {x:ℕ||ys||| ↑P[ys[x]]}  ~ ℕ||filter(P;ys)||
6. ↑(P y)
⊢ {x:ℕ||ys|| + 1| ↑P[ys @ [y][x]]}  ~ ℕ||filter(P;ys)|| + 1

2
1. [A] : Type
2. P : A ⟶ 𝔹
3. ys : A List
4. y : A
5. {x:ℕ||ys||| ↑P[ys[x]]}  ~ ℕ||filter(P;ys)||
6. ¬↑(P y)
⊢ {x:ℕ||ys|| + 1| ↑P[ys @ [y][x]]}  ~ ℕ||filter(P;ys)|| + 0

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  P  :  A  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  \mforall{}ys:A  List.  \mforall{}y:A.
        (\{x:\mBbbN{}||ys|||  \muparrow{}P[ys[x]]\}    \msim{}  \mBbbN{}||filter(P;ys)||
        {}\mRightarrow{}  \{x:\mBbbN{}||ys  @  [y]|||  \muparrow{}P[ys  @  [y][x]]\}    \msim{}  \mBbbN{}||filter(P;ys  @  [y])||)


By

---

Latex:
(Auto
  THEN  (RWO  "filter\_append"  0  THENA  Auto)
  THEN  (RWO  "length-append"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  SplitOnConclITE
  THEN  Auto
  THEN  Reduce  0)

---

Home Index