---

Step * of Lemma distinct-representatives

∀k:ℕ
  ∀[A:Type]
    (A ~ ℕk
    ⇒ (∀[E:A ⟶ A ⟶ ℙ]
          (EquivRel(A;x,y.E[x;y])
          ⇒ (∀x,y:A.  Dec(E[x;y]))
          ⇒ (∃L:A List. ((∀a,b∈L.  ¬E[a;b]) ∧ (∀a:A. (∃b∈L. E[a;b])) ∧ (||L|| ≤ k))))))
BY
{ TACTIC:(CompleteInductionOnNat
          THEN Auto
          THEN CaseNat 0 `k'
          THEN Try (((Assert ¬A BY (BLemma `equipollent-zero` THEN Complete (Auto))) THEN InstConcl [⌜[]⌝]⋅ THEN Auto))
          THEN (Assert ⌜A⌝⋅ BY
                      ((Assert ℕk ~ A BY (RelRST THEN Auto)) THEN D -1 THEN UseWitness ⌜f 0⌝⋅ THEN Auto))
          THEN RenameVar `b' (-1)
          THEN (InstLemma `equipollent-partition` [⌜k⌝;⌜A⌝;⌜λ2x.E[b;x]⌝]⋅ THENA Auto)
          THEN ExRepD) }

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

---

Latex:

---

Latex:
\mforall{}k:\mBbbN{}
    \mforall{}[A:Type]
        (A  \msim{}  \mBbbN{}k
        {}\mRightarrow{}  (\mforall{}[E:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}]
                    (EquivRel(A;x,y.E[x;y])
                    {}\mRightarrow{}  (\mforall{}x,y:A.    Dec(E[x;y]))
                    {}\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{}  (||L||  \mleq{}  k))))))


By

---

Latex:
TACTIC:(CompleteInductionOnNat
                THEN  Auto
                THEN  CaseNat  0  `k'
                THEN  Try  (((Assert  \mneg{}A  BY
                                                    (BLemma  `equipollent-zero`  THEN  Complete  (Auto)))
                                      THEN  InstConcl  [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}
                                      THEN  Auto))
                THEN  (Assert  \mkleeneopen{}A\mkleeneclose{}\mcdot{}  BY
                                        ((Assert  \mBbbN{}k  \msim{}  A  BY
                                                        (RelRST  THEN  Auto))
                                          THEN  D  -1
                                          THEN  UseWitness  \mkleeneopen{}f  0\mkleeneclose{}\mcdot{}
                                          THEN  Auto))
                THEN  RenameVar  `b'  (-1)
                THEN  (InstLemma  `equipollent-partition`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x.E[b;x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  ExRepD)

---

Home Index