---

Step * 1 2 of Lemma equipollent-distinct-representatives


1. [A] : Type
2. [E] : A ⟶ A ⟶ ℙ
3. EquivRel(A;x,y.E[x;y])
4. L : A List
5. (∀a,b∈L.  ¬E[a;b])
6. ∀a:A. (∃b∈L. E[a;b])
7. ∃f:A ⟶ ℕ||L||. ((∀a,b:A.  ((f a) = (f b) ∈ ℕ||L|| ⇐⇒ E[a;b])) ∧ (∀i:ℕ||L||. ∃a:A. ((f a) = i ∈ ℕ||L||)))
⊢ x,y:A//E[x;y] ~ ℕ||L||
BY
{ (D -1
   THEN (Assert f ∈ (x,y:A//E[x;y]) ⟶ ℕ||L|| BY
               (ExtWith [`z'] [⌜A ⟶ ℕ||L||⌝]⋅ THEN Try (Complete (Auto)) THEN D -1 THEN Auto))
   ) }

1
1. [A] : Type
2. [E] : A ⟶ A ⟶ ℙ
3. EquivRel(A;x,y.E[x;y])
4. L : A List
5. (∀a,b∈L.  ¬E[a;b])
6. ∀a:A. (∃b∈L. E[a;b])
7. f : A ⟶ ℕ||L||
8. (∀a,b:A.  ((f a) = (f b) ∈ ℕ||L|| ⇐⇒ E[a;b])) ∧ (∀i:ℕ||L||. ∃a:A. ((f a) = i ∈ ℕ||L||))
9. f ∈ (x,y:A//E[x;y]) ⟶ ℕ||L||
⊢ x,y:A//E[x;y] ~ ℕ||L||

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [E]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  EquivRel(A;x,y.E[x;y])
4.  L  :  A  List
5.  (\mforall{}a,b\mmember{}L.    \mneg{}E[a;b])
6.  \mforall{}a:A.  (\mexists{}b\mmember{}L.  E[a;b])
7.  \mexists{}f:A  {}\mrightarrow{}  \mBbbN{}||L||.  ((\mforall{}a,b:A.    ((f  a)  =  (f  b)  \mLeftarrow{}{}\mRightarrow{}  E[a;b]))  \mwedge{}  (\mforall{}i:\mBbbN{}||L||.  \mexists{}a:A.  ((f  a)  =  i)))
\mvdash{}  x,y:A//E[x;y]  \msim{}  \mBbbN{}||L||


By

---

Latex:
(D  -1
  THEN  (Assert  f  \mmember{}  (x,y:A//E[x;y])  {}\mrightarrow{}  \mBbbN{}||L||  BY
                          (ExtWith  [`z']  [\mkleeneopen{}A  {}\mrightarrow{}  \mBbbN{}||L||\mkleeneclose{}]\mcdot{}  THEN  Try  (Complete  (Auto))  THEN  D  -1  THEN  Auto))
  )

---

Home Index