---

Step * of Lemma count-by-decidable-equiv

∀[A:Type]. ∀[E:A ⟶ A ⟶ ℙ].
  (EquivRel(A;x,y.E[x;y])
  ⇒ (∀x,y:A.  Dec(E[x;y]))
  ⇒ (∀k:ℕ
        (A ~ ℕk
        ⇒ (∃L:A List
             ((∀a,b∈L.  ¬E[a;b])
             ∧ (∀a:A. (∃b∈L. E[a;b]))
             ∧ (∃f:ℕ||L|| ⟶ ℕ. ((∀i:ℕ||L||. {a:A| E[a;L[i]]}  ~ ℕf i) ∧ A ~ i:ℕ||L|| × ℕf i ∧ (k = Σ(f i | i < ||L||) ∈\000C ℤ))))))))
BY
{ (Auto
   THEN (InstLemma `distinct-representatives` [⌜k⌝;⌜A⌝;⌜E⌝]⋅ THENA Auto)
   THEN ParallelLast
   THEN Auto
   THEN Try ((BackThruSomeHyp THEN Auto))) }

1
1. [A] : Type
2. [E] : A ⟶ A ⟶ ℙ
3. EquivRel(A;x,y.E[x;y])
4. ∀x,y:A.  Dec(E[x;y])
5. k : ℕ
6. A ~ ℕk
7. L : A List
8. (∀a,b∈L.  ¬E[a;b])
9. ∀a:A. (∃b∈L. E[a;b])
10. ||L|| ≤ k
11. (∀a,b∈L.  ¬E[a;b])
12. ∀a:A. (∃b∈L. E[a;b])
⊢ ∃f:ℕ||L|| ⟶ ℕ. ((∀i:ℕ||L||. {a:A| E[a;L[i]]}  ~ ℕf i) ∧ A ~ i:ℕ||L|| × ℕf i ∧ (k = Σ(f i | i < ||L||) ∈ ℤ))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (InstLemma  `distinct-representatives`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}E\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  ParallelLast
  THEN  Auto
  THEN  Try  ((BackThruSomeHyp  THEN  Auto)))

---

Home Index