---

Step * 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)
⊢ map(f;remove-repeats-fun(eq;f;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
{ ((InstLemma `remove-repeats-fun-as-filter` [⌜{x:T| ↑(P x)} ⌝;⌜U⌝;⌜eq⌝;⌜f⌝;⌜R⌝;⌜filter(P;L)⌝]⋅
    THENA (Auto
           THEN Try ((BLemma `sorted-by-filter` THEN Auto))
           THEN Try (Complete (RepeatFor 2 (ParallelOp -3)))
           THEN Try (Complete ((RepeatFor 2 (ParallelOp -2) THEN ParallelLast))))
    )
   THEN RWO "-1" 0
   )⋅ }

1
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)

---

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)
\mvdash{}  map(f;remove-repeats-fun(eq;f;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:
((InstLemma  `remove-repeats-fun-as-filter`  [\mkleeneopen{}\{x:T|  \muparrow{}(P  x)\}  \mkleeneclose{};\mkleeneopen{}U\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}R\mkleeneclose{};\mkleeneopen{}filter(P;L)\mkleeneclose{}]\mcdot{}
    THENA  (Auto
                  THEN  Try  ((BLemma  `sorted-by-filter`  THEN  Auto))
                  THEN  Try  (Complete  (RepeatFor  2  (ParallelOp  -3)))
                  THEN  Try  (Complete  ((RepeatFor  2  (ParallelOp  -2)  THEN  ParallelLast))))
    )
  THEN  RWO  "-1"  0
  )\mcdot{}

---

Home Index