---

Step * of Lemma list-to-set-filter

∀[T:Type]. ∀eq:EqDecider(T). ∀P:T ⟶ 𝔹. ∀L:T List.  (list-to-set(eq;filter(P;L)) ~ filter(P;list-to-set(eq;L)))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN (RWO "list-to-set-cons" 0 THENA Auto)
   THEN Repeat (AutoSplit)
   THEN (RWO "list-to-set-cons" 0 THENA Auto)
   THEN RWO "-3" 0
   THEN AutoSplit) }

1
1. T : Type
2. eq : EqDecider(T)
3. P : T ⟶ 𝔹
4. u : T
5. v : T List
6. ¬(u ∈ filter(P;list-to-set(eq;v)))
7. list-to-set(eq;filter(P;v)) ~ filter(P;list-to-set(eq;v))
8. ↑(P u)
9. (u ∈ list-to-set(eq;v))
⊢ [u / filter(P;list-to-set(eq;v))] ~ filter(P;list-to-set(eq;v))

2
1. T : Type
2. eq : EqDecider(T)
3. P : T ⟶ 𝔹
4. u : T
5. v : T List
6. ¬(u ∈ list-to-set(eq;v))
7. list-to-set(eq;filter(P;v)) ~ filter(P;list-to-set(eq;v))
8. ↑(P u)
9. ↑(P u)
10. (u ∈ filter(P;list-to-set(eq;v)))
⊢ filter(P;list-to-set(eq;v)) ~ [u / filter(P;list-to-set(eq;v))]

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}L:T  List.
        (list-to-set(eq;filter(P;L))  \msim{}  filter(P;list-to-set(eq;L)))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "list-to-set-cons"  0  THENA  Auto)
  THEN  Repeat  (AutoSplit)
  THEN  (RWO  "list-to-set-cons"  0  THENA  Auto)
  THEN  RWO  "-3"  0
  THEN  AutoSplit)

---

Home Index