---

Step * of Lemma l_disjoint-representatives

∀[T:Type]
  ((∀x,y:T.  Dec(x = y ∈ T))
  ⇒ (∀L:T List List
        ∃reps:T List List
         (reps ⊆ L ∧ (∀as∈L.(∃rep∈reps. ¬l_disjoint(T;as;rep))) ∧ (∀rep1,rep2∈reps.  l_disjoint(T;rep1;rep2))) 
        supposing (∀as∈L.0 < ||as||)))
BY
{ ((Unfold `pairwise` 0 THEN InductionOnList) THEN Auto THEN Try (Complete ((InstConcl [⌜[]⌝]⋅ THEN Auto')))) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. u : T List
4. v : T List List
5. ∃reps:T List List
    (reps ⊆ v ∧ (∀as∈v.(∃rep∈reps. ¬l_disjoint(T;as;rep))) ∧ (∀i:ℕ||reps||. ∀j:ℕi.  l_disjoint(T;reps[j];reps[i]))) 
   supposing (∀as∈v.0 < ||as||)
6. (∀as∈[u / v].0 < ||as||)
⊢ ∃reps:T List List
   (reps ⊆ [u / v]
   ∧ (∀as∈[u / v].(∃rep∈reps. ¬l_disjoint(T;as;rep)))
   ∧ (∀i:ℕ||reps||. ∀j:ℕi.  l_disjoint(T;reps[j];reps[i])))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    ((\mforall{}x,y:T.    Dec(x  =  y))
    {}\mRightarrow{}  (\mforall{}L:T  List  List
                \mexists{}reps:T  List  List
                  (reps  \msubseteq{}  L
                  \mwedge{}  (\mforall{}as\mmember{}L.(\mexists{}rep\mmember{}reps.  \mneg{}l\_disjoint(T;as;rep)))
                  \mwedge{}  (\mforall{}rep1,rep2\mmember{}reps.    l\_disjoint(T;rep1;rep2))) 
                supposing  (\mforall{}as\mmember{}L.0  <  ||as||)))


By

---

Latex:
((Unfold  `pairwise`  0  THEN  InductionOnList)
  THEN  Auto
  THEN  Try  (Complete  ((InstConcl  [\mkleeneopen{}[]\mkleeneclose{}]\mcdot{}  THEN  Auto'))))

---

Home Index