Step * 2 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 (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
BY
{ (D (-2) THEN RWO "l_exists_cons" 0 THEN Auto) }

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{}  (eqof(eq)  (f  x)  (f  a)))\_b);v)
14.  x  :  A
15.  (x  \mmember{}  v)
16.  \mneg{}(\mexists{}x@0\mmember{}[u  /  v].  (\muparrow{}R[x@0;x])  \mwedge{}  ((f  x@0)  =  (f  x)))
17.  (\mexists{}x@0\mmember{}v.  (\muparrow{}R[x@0;x])  \mwedge{}  ((f  x@0)  =  (f  x)))
\mvdash{}  False


By

Latex:
(D  (-2)  THEN  RWO  "l\_exists\_cons"  0  THEN  Auto)



Home Index