---

Step * 1 of Lemma l_disjoint-representatives


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])))
BY
{ ((RWO "l_all_cons" (-1) THENA Auto) THEN (D (-2) THENA Auto) THEN ExRepD) }

1
1. [T] : Type
2. ∀x,y:T.  Dec(x = y ∈ T)
3. u : T List
4. v : T List List
5. 0 < ||u||
6. (∀as∈v.0 < ||as||)
7. reps : T List List
8. reps ⊆ v
9. (∀as∈v.(∃rep∈reps. ¬l_disjoint(T;as;rep)))
10. ∀i:ℕ||reps||. ∀j:ℕi.  l_disjoint(T;reps[j];reps[i])
⊢ ∃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:

1.  [T]  :  Type
2.  \mforall{}x,y:T.    Dec(x  =  y)
3.  u  :  T  List
4.  v  :  T  List  List
5.  \mexists{}reps:T  List  List
        (reps  \msubseteq{}  v
        \mwedge{}  (\mforall{}as\mmember{}v.(\mexists{}rep\mmember{}reps.  \mneg{}l\_disjoint(T;as;rep)))
        \mwedge{}  (\mforall{}i:\mBbbN{}||reps||.  \mforall{}j:\mBbbN{}i.    l\_disjoint(T;reps[j];reps[i]))) 
      supposing  (\mforall{}as\mmember{}v.0  <  ||as||)
6.  (\mforall{}as\mmember{}[u  /  v].0  <  ||as||)
\mvdash{}  \mexists{}reps:T  List  List
      (reps  \msubseteq{}  [u  /  v]
      \mwedge{}  (\mforall{}as\mmember{}[u  /  v].(\mexists{}rep\mmember{}reps.  \mneg{}l\_disjoint(T;as;rep)))
      \mwedge{}  (\mforall{}i:\mBbbN{}||reps||.  \mforall{}j:\mBbbN{}i.    l\_disjoint(T;reps[j];reps[i])))


By

---

Latex:
((RWO  "l\_all\_cons"  (-1)  THENA  Auto)  THEN  (D  (-2)  THENA  Auto)  THEN  ExRepD)

---

Home Index