---

Step * of Lemma remove-repeats-fun-map2

∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[L:A List]. ∀[f:{a:A| (a ∈ L)}  ⟶ B].
  (map(f;remove-repeats-fun(eq;f;L)) = remove-repeats(eq;map(f;L)) ∈ (B List))
BY
{ (InductionOnList
   THEN RepUR ``remove-repeats-fun`` 0
   THEN Try (Complete (Auto))
   THEN Try (Fold `remove-repeats-fun` 0)
   THEN (UnivCD THENA Auto)
   THEN (EqCD THEN Auto)
   THEN (Assert map(f;filter(λx.(¬b(eq (f x) (f u)));remove-repeats-fun(eq;f;v)))
               = filter(λx.(¬b(eq x (f u)));map(f;remove-repeats-fun(eq;f;v)))
               ∈ (B List) BY
               ((RWO "filter-map" 0 THENA Auto)
                THEN RepUR ``compose`` 0
                THEN Auto
                THEN (InstLemma `list-set-type` [⌜A⌝;⌜v⌝]⋅ THENA Auto)
                THEN DoSubsume⋅
                THEN Auto))
   THEN NthHypEqTrans (-1)) }

1
.....assertion..... 
1. A : Type
2. B : Type
3. eq : EqDecider(B)
4. u : A
5. v : A List
6. ∀[f:{a:A| (a ∈ v)}  ⟶ B]. (map(f;remove-repeats-fun(eq;f;v)) = remove-repeats(eq;map(f;v)) ∈ (B List))
7. f : {a:A| (a ∈ [u / v])}  ⟶ B
8. map(f;filter(λx.(¬b(eq (f x) (f u)));remove-repeats-fun(eq;f;v)))
= filter(λx.(¬b(eq x (f u)));map(f;remove-repeats-fun(eq;f;v)))
∈ (B List)
⊢ filter(λx.(¬b(eq x (f u)));map(f;remove-repeats-fun(eq;f;v)))
= filter(λx.(¬b(eq x (f u)));remove-repeats(eq;map(f;v)))
∈ (B List)

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[eq:EqDecider(B)].  \mforall{}[L:A  List].  \mforall{}[f:\{a:A|  (a  \mmember{}  L)\}    {}\mrightarrow{}  B].
    (map(f;remove-repeats-fun(eq;f;L))  =  remove-repeats(eq;map(f;L)))


By

---

Latex:
(InductionOnList
  THEN  RepUR  ``remove-repeats-fun``  0
  THEN  Try  (Complete  (Auto))
  THEN  Try  (Fold  `remove-repeats-fun`  0)
  THEN  (UnivCD  THENA  Auto)
  THEN  (EqCD  THEN  Auto)
  THEN  (Assert  map(f;filter(\mlambda{}x.(\mneg{}\msubb{}(eq  (f  x)  (f  u)));remove-repeats-fun(eq;f;v)))
                          =  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  (f  u)));map(f;remove-repeats-fun(eq;f;v)))  BY
                          ((RWO  "filter-map"  0  THENA  Auto)
                            THEN  RepUR  ``compose``  0
                            THEN  Auto
                            THEN  (InstLemma  `list-set-type`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  DoSubsume\mcdot{}
                            THEN  Auto))
  THEN  NthHypEqTrans  (-1))

---

Home Index