---

Step * 1 1 2 3 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. 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])
11. ¬(∃rep∈reps. ¬l_disjoint(T;u;rep))
12. [u / reps] ⊆ [u / v]
13. (∀as∈[u / v].(∃rep∈[u / reps]. ¬l_disjoint(T;as;rep)))
14. i : ℕ||[u / reps]||
15. j : ℕi
⊢ l_disjoint(T;[u / reps][j];[u / reps][i])
BY
{ (Assert (∀rep1,rep2∈[u / reps].  l_disjoint(T;rep1;rep2)) BY
         ((BLemma `pairwise-cons` THEN Auto)
          THEN D 0
          THEN Auto
          THEN SupposeNot
          THEN D -8
          THEN With ⌜i1⌝ (D 0)⋅
          THEN Auto)) }

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])
11. ¬(∃rep∈reps. ¬l_disjoint(T;u;rep))
12. [u / reps] ⊆ [u / v]
13. (∀as∈[u / v].(∃rep∈[u / reps]. ¬l_disjoint(T;as;rep)))
14. i : ℕ||[u / reps]||
15. j : ℕi
16. (∀rep1,rep2∈[u / reps].  l_disjoint(T;rep1;rep2))
⊢ l_disjoint(T;[u / reps][j];[u / 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.  0  <  ||u||
6.  (\mforall{}as\mmember{}v.0  <  ||as||)
7.  reps  :  T  List  List
8.  reps  \msubseteq{}  v
9.  (\mforall{}as\mmember{}v.(\mexists{}rep\mmember{}reps.  \mneg{}l\_disjoint(T;as;rep)))
10.  \mforall{}i:\mBbbN{}||reps||.  \mforall{}j:\mBbbN{}i.    l\_disjoint(T;reps[j];reps[i])
11.  \mneg{}(\mexists{}rep\mmember{}reps.  \mneg{}l\_disjoint(T;u;rep))
12.  [u  /  reps]  \msubseteq{}  [u  /  v]
13.  (\mforall{}as\mmember{}[u  /  v].(\mexists{}rep\mmember{}[u  /  reps].  \mneg{}l\_disjoint(T;as;rep)))
14.  i  :  \mBbbN{}||[u  /  reps]||
15.  j  :  \mBbbN{}i
\mvdash{}  l\_disjoint(T;[u  /  reps][j];[u  /  reps][i])


By

---

Latex:
(Assert  (\mforall{}rep1,rep2\mmember{}[u  /  reps].    l\_disjoint(T;rep1;rep2))  BY
              ((BLemma  `pairwise-cons`  THEN  Auto)
                THEN  D  0
                THEN  Auto
                THEN  SupposeNot
                THEN  D  -8
                THEN  With  \mkleeneopen{}i1\mkleeneclose{}  (D  0)\mcdot{}
                THEN  Auto))

---

Home Index