---

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

∀[T,U:Type]. ∀[eq:EqDecider(U)]. ∀[R:T ⟶ T ⟶ 𝔹]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| ↑(P x)}  ⟶ U].
  (remove-repeats(eq;mapfilter(f;P;L))
     = mapfilter(f;λa.((P a) ∧b (¬b(∃x∈L.(P x) ∧b R[x;a] ∧b (eq (f x) (f a)))_b));L)
     ∈ (U List)) supposing 
     (sorted-by(λx,y. (↑R[x;y]);L) and 
     StAntiSym(T;x,y.↑R[x;y]) and 
     Irrefl(T;x,y.↑R[x;y]))
BY
{ (Auto
   THEN Unfold `mapfilter` 0
   THEN (RWO "remove-repeats-fun-map2<" 0
         THENA (Try (Complete (Auto))
                THEN Try (Complete ((DoSubsume THEN Auto THEN SubtypeReasoning THEN Auto THEN RW ListC (-1) THEN Auto)))
                THEN Using [`A',⌜{a:T| ↑((P a) ∧b (¬b(∃x∈L.(P x) ∧b R[x;a] ∧b (eq (f x) (f a)))_b))} ⌝] EqCD⋅⋅
                THEN Try (BLemma `filter_type`)
                THEN Auto)
         )) }

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

---

Latex:

---

Latex:
\mforall{}[T,U:Type].  \mforall{}[eq:EqDecider(U)].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].
\mforall{}[f:\{x:T|  \muparrow{}(P  x)\}    {}\mrightarrow{}  U].
    (remove-repeats(eq;mapfilter(f;P;L))
          =  mapfilter(f;\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))  supposing 
          (sorted-by(\mlambda{}x,y.  (\muparrow{}R[x;y]);L)  and 
          StAntiSym(T;x,y.\muparrow{}R[x;y])  and 
          Irrefl(T;x,y.\muparrow{}R[x;y]))


By

---

Latex:
(Auto
  THEN  Unfold  `mapfilter`  0
  THEN  (RWO  "remove-repeats-fun-map2<"  0
              THENA  (Try  (Complete  (Auto))
                            THEN  Try  (Complete  ((DoSubsume
                                                                      THEN  Auto
                                                                      THEN  SubtypeReasoning
                                                                      THEN  Auto
                                                                      THEN  RW  ListC  (-1)
                                                                      THEN  Auto)))
                            THEN  Using  [`A',\mkleeneopen{}\{a:T|  \muparrow{}((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))\}  \mkleeneclose{}
                            ]  EqCD\mcdot{}\mcdot{}
                            THEN  Try  (BLemma  `filter\_type`)
                            THEN  Auto)
              ))

---

Home Index