---

Step * 1 1 1 1 of Lemma equipollent-distinct-representatives

.....assertion..... 
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. ∃i:ℕ||L||. E[a;L[i]]
7. rep : a:A ⟶ ℕ||L||
8. ∀a:A. E[a;L[rep a]]
⊢ ∀i,j:ℕ||L||.  (E[L[i];L[j]] ⇒ (i = j ∈ ℤ))
BY
{ (Auto
   THEN (Decide ⌜i < j⌝⋅ THENA Auto)
   THEN Try (((With ⌜j⌝ (D 5)⋅ THENM With ⌜i⌝ (D (-1))⋅) THEN Complete (Auto))⋅)
   THEN (Decide ⌜j < i⌝⋅ THENA Auto)
   THEN Auto'
   THEN (With ⌜i⌝ (D 5)⋅ THENM With ⌜j⌝ (D (-1))⋅)
   THEN Auto
   THEN D -1
   THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
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{}i:\mBbbN{}||L||.  E[a;L[i]]
7.  rep  :  a:A  {}\mrightarrow{}  \mBbbN{}||L||
8.  \mforall{}a:A.  E[a;L[rep  a]]
\mvdash{}  \mforall{}i,j:\mBbbN{}||L||.    (E[L[i];L[j]]  {}\mRightarrow{}  (i  =  j))


By

---

Latex:
(Auto
  THEN  (Decide  \mkleeneopen{}i  <  j\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Try  (((With  \mkleeneopen{}j\mkleeneclose{}  (D  5)\mcdot{}  THENM  With  \mkleeneopen{}i\mkleeneclose{}  (D  (-1))\mcdot{})  THEN  Complete  (Auto))\mcdot{})
  THEN  (Decide  \mkleeneopen{}j  <  i\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Auto'
  THEN  (With  \mkleeneopen{}i\mkleeneclose{}  (D  5)\mcdot{}  THENM  With  \mkleeneopen{}j\mkleeneclose{}  (D  (-1))\mcdot{})
  THEN  Auto
  THEN  D  -1
  THEN  Auto)

---

Home Index