---

Step * 1 1 2 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. 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))
⊢ [u / reps] ⊆ [u / v]
BY
{ (BLemma `l_contains_cons`
   THEN Auto
   THEN (Using [`B',⌜v⌝] (BLemma `l_contains_transitivity`)⋅
         THEN Auto
         THEN Subst ⌜[u / v] ~ [u] @ v⌝ 0⋅
         THEN Try ((BLemma `l_contains_append2` THEN Auto))
         THEN Reduce 0
         THEN Auto)⋅) }

---

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))
\mvdash{}  [u  /  reps]  \msubseteq{}  [u  /  v]


By

---

Latex:
(BLemma  `l\_contains\_cons`
  THEN  Auto
  THEN  (Using  [`B',\mkleeneopen{}v\mkleeneclose{}]  (BLemma  `l\_contains\_transitivity`)\mcdot{}
              THEN  Auto
              THEN  Subst  \mkleeneopen{}[u  /  v]  \msim{}  [u]  @  v\mkleeneclose{}  0\mcdot{}
              THEN  Try  ((BLemma  `l\_contains\_append2`  THEN  Auto))
              THEN  Reduce  0
              THEN  Auto)\mcdot{})

---

Home Index