---

Step * 1 of Lemma remove-repeats-fun-map2

.....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)
BY
{ ((GenConclTerm ⌜f u⌝⋅ THENA Auto)
   THEN (D 6 With ⌜f⌝  THENA Auto)
   THEN ApFunToHypEquands `Z' ⌜filter(λx.(¬b(eq x v1));Z)⌝ ⌜B List⌝ (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  A  :  Type
2.  B  :  Type
3.  eq  :  EqDecider(B)
4.  u  :  A
5.  v  :  A  List
6.  \mforall{}[f:\{a:A|  (a  \mmember{}  v)\}    {}\mrightarrow{}  B].  (map(f;remove-repeats-fun(eq;f;v))  =  remove-repeats(eq;map(f;v)))
7.  f  :  \{a:A|  (a  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  B
8.  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)))
\mvdash{}  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  (f  u)));map(f;remove-repeats-fun(eq;f;v)))
=  filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  (f  u)));remove-repeats(eq;map(f;v)))


By

---

Latex:
((GenConclTerm  \mkleeneopen{}f  u\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (D  6  With  \mkleeneopen{}f\mkleeneclose{}    THENA  Auto)
  THEN  ApFunToHypEquands  `Z'  \mkleeneopen{}filter(\mlambda{}x.(\mneg{}\msubb{}(eq  x  v1));Z)\mkleeneclose{}  \mkleeneopen{}B  List\mkleeneclose{}  (-1)\mcdot{}
  THEN  Auto)

---

Home Index