---

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


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)]
BY
{ (EqCD
   THEN Try (Complete (Auto))
   THEN BLemma `filter-sq`
   THEN AllReduce
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN ExRepD
   THEN DVarSets
   THEN (All(RW assert_pushdownC) THENA Auto)) }

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. ¬(∃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 (eqof(eq) (f x) (f a)))_b);v)
14. x : A
15. (x ∈ v)
16. (¬(∃x@0∈v. (↑R[x@0;x]) ∧ ((f x@0) = (f x) ∈ B))) ∧ (¬((f x) = (f u) ∈ B))
17. (∃x@0∈[u / v]. (↑R[x@0;x]) ∧ ((f x@0) = (f x) ∈ B))
⊢ False

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 (eqof(eq) (f x) (f a)))_b);v)
14. x : A
15. (x ∈ v)
16. ¬(∃x@0∈[u / v]. (↑R[x@0;x]) ∧ ((f x@0) = (f x) ∈ B))
17. (∃x@0∈v. (↑R[x@0;x]) ∧ ((f x@0) = (f x) ∈ B))
⊢ False

3
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 (eqof(eq) (f x) (f a)))_b);v)
14. x : A
15. (x ∈ v)
16. ¬(∃x@0∈[u / v]. (↑R[x@0;x]) ∧ ((f x@0) = (f x) ∈ B))
17. ¬(∃x@0∈v. (↑R[x@0;x]) ∧ ((f x@0) = (f x) ∈ B))
18. (f x) = (f u) ∈ B
⊢ False

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  eq  :  EqDecider(B)
4.  f  :  A  {}\mrightarrow{}  B
5.  R  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}
6.  u  :  A
7.  v  :  A  List
8.  \mneg{}(\mexists{}x\mmember{}[u  /  v].  (\muparrow{}R[x;u])  \mwedge{}  ((f  x)  =  (f  u)))
9.  Irrefl(A;x,y.\muparrow{}R[x;y])
10.  StAntiSym(A;x,y.\muparrow{}R[x;y])
11.  sorted-by(\mlambda{}x,y.  (\muparrow{}R[x;y]);v)
12.  (\mforall{}z\mmember{}v.\muparrow{}R[u;z])
13.  remove-repeats-fun(eq;f;v)  \msim{}  filter(\mlambda{}a.(\mneg{}\msubb{}(\mexists{}x\mmember{}v.R[x;a]  \mwedge{}\msubb{}  (eq  (f  x)  (f  a)))\_b);v)
\mvdash{}  [u  /  filter(\mlambda{}t.((\mneg{}\msubb{}(\mexists{}x\mmember{}v.R[x;t]  \mwedge{}\msubb{}  (eq  (f  x)  (f  t)))\_b)  \mwedge{}\msubb{}  (\mneg{}\msubb{}(eq  (f  t)  (f  u))));v)] 
\msim{}  [u  /  filter(\mlambda{}a.(\mneg{}\msubb{}(\mexists{}x\mmember{}[u  /  v].R[x;a]  \mwedge{}\msubb{}  (eq  (f  x)  (f  a)))\_b);v)]


By

---

Latex:
(EqCD
  THEN  Try  (Complete  (Auto))
  THEN  BLemma  `filter-sq`
  THEN  AllReduce
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD
  THEN  DVarSets
  THEN  (All(RW  assert\_pushdownC)  THENA  Auto))

---

Home Index