---

Step * 1 1 of Lemma remove-repeats-mapfilter-with-fun


1. T : Type
2. U : Type
3. eq : EqDecider(U)
4. R : T ⟶ T ⟶ 𝔹
5. L : T List
6. P : T ⟶ 𝔹
7. f : {x:T| ↑(P x)}  ⟶ U
8. Irrefl(T;x,y.↑R[x;y])
9. StAntiSym(T;x,y.↑R[x;y])
10. sorted-by(λx,y. (↑R[x;y]);L)
11. remove-repeats-fun(eq;f;filter(P;L)) ~ filter(λa.(¬b(∃x∈filter(P;L).R[x;a] ∧b (eq (f x) (f a)))_b);filter(P;L))
⊢ map(f;filter(λa.(¬b(∃x∈filter(P;L).R[x;a] ∧b (eq (f x) (f a)))_b);filter(P;L)))
= map(f;filter(λa.((P a) ∧b (¬b(∃x∈L.(P x) ∧b R[x;a] ∧b (eq (f x) (f a)))_b));L))
∈ (U List)
BY
{ ((RWO "filter-filter" 0 THENA Auto)
   THEN Reduce 0
   THEN (RWO "bl-exists-filter" 0 THENA MemTop)
   THEN Fold `member` 0
   THEN Fold `mapfilter` 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  U  :  Type
3.  eq  :  EqDecider(U)
4.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}
5.  L  :  T  List
6.  P  :  T  {}\mrightarrow{}  \mBbbB{}
7.  f  :  \{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  U
8.  Irrefl(T;x,y.\muparrow{}R[x;y])
9.  StAntiSym(T;x,y.\muparrow{}R[x;y])
10.  sorted-by(\mlambda{}x,y.  (\muparrow{}R[x;y]);L)
11.  remove-repeats-fun(eq;f;filter(P;L)) 
\msim{}  filter(\mlambda{}a.(\mneg{}\msubb{}(\mexists{}x\mmember{}filter(P;L).R[x;a]  \mwedge{}\msubb{}  (eq  (f  x)  (f  a)))\_b);filter(P;L))
\mvdash{}  map(f;filter(\mlambda{}a.(\mneg{}\msubb{}(\mexists{}x\mmember{}filter(P;L).R[x;a]  \mwedge{}\msubb{}  (eq  (f  x)  (f  a)))\_b);filter(P;L)))
=  map(f;filter(\mlambda{}a.((P  a)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(\mexists{}x\mmember{}L.(P  x)  \mwedge{}\msubb{}  R[x;a]  \mwedge{}\msubb{}  (eq  (f  x)  (f  a)))\_b));L))


By

---

Latex:
((RWO  "filter-filter"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (RWO  "bl-exists-filter"  0  THENA  MemTop)
  THEN  Fold  `member`  0
  THEN  Fold  `mapfilter`  0
  THEN  Auto)\mcdot{}

---

Home Index