---

Step * of Lemma remove-repeats-fun-as-filter

∀[A,B:Type]. ∀[eq:EqDecider(B)]. ∀[f:A ⟶ B]. ∀[R:A ⟶ A ⟶ 𝔹]. ∀[L:A List].
  (remove-repeats-fun(eq;f;L) ~ filter(λa.(¬b(∃x∈L.R[x;a] ∧b (eq (f x) (f a)))_b);L)) supposing 
     (sorted-by(λx,y. (↑R[x;y]);L) and 
     StAntiSym(A;x,y.↑R[x;y]) and 
     Irrefl(A;x,y.↑R[x;y]))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN (UnivCD THENA Auto)
   THEN Unfold `remove-repeats-fun` 0
   THEN Reduce 0
   THEN Try (CpltAuto)
   THEN Try (Fold `remove-repeats-fun` 0)
   THEN (RW ListC (-1) THENA Auto)
   THEN AllReduce
   THEN RepD
   THEN (D (-5) THENA Auto)
   THEN RepeatFor 2 ((D (-1) THENA Auto))
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN (RWO "filter-filter" 0 THENA Auto)
   THEN Reduce 0
   THEN AutoSplit) }

1
1. A : Type
2. B : Type
3. eq : EqDecider(B)
4. f : A ⟶ B
5. R : A ⟶ A ⟶ 𝔹
6. u : A
7. v : A List
8. Irrefl(A;x,y.↑R[x;y])
9. StAntiSym(A;x,y.↑R[x;y])
10. sorted-by(λx,y. (↑R[x;y]);v)
11. (∀z∈v.↑R[u;z])
12. remove-repeats-fun(eq;f;v) ~ filter(λa.(¬b(∃x∈v.R[x;a] ∧b (eq (f x) (f a)))_b);v)
13. (∃x∈[u / v]. (↑R[x;u]) ∧ ((f x) = (f u) ∈ B))
⊢ [u / filter(λt.((¬b(∃x∈v.R[x;t] ∧b (eq (f x) (f t)))_b) ∧b (¬b(eq (f t) (f u))));v)] ~ filter(λa.(¬b(∃x∈[u / v].R[x;a]
                                                                                                         ∧b (eq (f x) 
                                                                                                             (f a)))_b);
                                                                                                v)

2
1. A : Type
2. B : Type
3. eq : EqDecider(B)
4. f : A ⟶ B
5. R : A ⟶ A ⟶ 𝔹
6. u : A
7. v : A List
8. ¬(∃x∈[u / v]. (↑R[x;u]) ∧ ((f x) = (f u) ∈ B))
9. Irrefl(A;x,y.↑R[x;y])
10. StAntiSym(A;x,y.↑R[x;y])
11. sorted-by(λx,y. (↑R[x;y]);v)
12. (∀z∈v.↑R[u;z])
13. remove-repeats-fun(eq;f;v) ~ filter(λa.(¬b(∃x∈v.R[x;a] ∧b (eq (f x) (f a)))_b);v)
⊢ [u / filter(λt.((¬b(∃x∈v.R[x;t] ∧b (eq (f x) (f t)))_b) ∧b (¬b(eq (f t) (f u))));v)] ~ [u / 
                                                                                          filter(λa.(¬b(∃x∈[u / v].
                                                                                                          R[x;a]
                                                                                                          ∧b (eq (f x) 
                                                                                                              (f 
                                                                                                               a)))_b);
                                                                                                 v)]

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[eq:EqDecider(B)].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[R:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].
    (remove-repeats-fun(eq;f;L)  \msim{}  filter(\mlambda{}a.(\mneg{}\msubb{}(\mexists{}x\mmember{}L.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(A;x,y.\muparrow{}R[x;y])  and 
          Irrefl(A;x,y.\muparrow{}R[x;y]))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Unfold  `remove-repeats-fun`  0
  THEN  Reduce  0
  THEN  Try  (CpltAuto)
  THEN  Try  (Fold  `remove-repeats-fun`  0)
  THEN  (RW  ListC  (-1)  THENA  Auto)
  THEN  AllReduce
  THEN  RepD
  THEN  (D  (-5)  THENA  Auto)
  THEN  RepeatFor  2  ((D  (-1)  THENA  Auto))
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  (RWO  "filter-filter"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  AutoSplit)

---

Home Index