---

Step * of Lemma count-by-equiv

∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
  (EquivRel(A;x,y.E[x;y])
  ⇒ (∀L:A List. (∀a:A. (∃b∈L. E[a;b])) ⇒ A ~ i:ℕ||L|| × {a:A| E[a;L[i]]}  supposing (∀a,b∈L.  ¬E[a;b])))
BY
{ (Auto
   THEN (RWO "l_exists_iff" (-1) THENA Auto)
   THEN (Skolemize (-1) `rep' THENA Auto)
   THEN (Assert ∀a:A. (rep a ∈ L) BY
               Auto)
   THEN Unfold `l_member` -1
   THEN Skolemize (-1) `f'
   THEN Auto
   THEN All (Unfold `cand`)
   THEN All (Fold `and`)) }

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:A. ((b ∈ L) ∧ E[a;b])
7. rep : a:A ⟶ A
8. ∀a:A. ((rep a ∈ L) ∧ E[a;rep a])
9. ∀a:A. ∃i:ℕ. (i < ||L|| ∧ ((rep a) = L[i] ∈ A))
10. f : a:A ⟶ ℕ
11. ∀a:A. (f a < ||L|| ∧ ((rep a) = L[f a] ∈ A))
⊢ A ~ i:ℕ||L|| × {a:A| E[a;L[i]]} 

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    (EquivRel(A;x,y.E[x;y])
    {}\mRightarrow{}  (\mforall{}L:A  List
                (\mforall{}a:A.  (\mexists{}b\mmember{}L.  E[a;b]))  {}\mRightarrow{}  A  \msim{}  i:\mBbbN{}||L||  \mtimes{}  \{a:A|  E[a;L[i]]\}    supposing  (\mforall{}a,b\mmember{}L.    \mneg{}E[a;b])))


By

---

Latex:
(Auto
  THEN  (RWO  "l\_exists\_iff"  (-1)  THENA  Auto)
  THEN  (Skolemize  (-1)  `rep'  THENA  Auto)
  THEN  (Assert  \mforall{}a:A.  (rep  a  \mmember{}  L)  BY
                          Auto)
  THEN  Unfold  `l\_member`  -1
  THEN  Skolemize  (-1)  `f'
  THEN  Auto
  THEN  All  (Unfold  `cand`)
  THEN  All  (Fold  `and`))

---

Home Index