---

Step * 2 of Lemma sub-bag-list-if-bag-no-repeats-sq


1. A : Type
2. u : A
3. v : A List
4. ∀bs:A List. (no_repeats(A;v) ⇒ (∀x∈v.(x ∈ bs)) ⇒ (↓sub-bag(A;v;bs)))
5. bs : A List
6. no_repeats(A;v)
7. ¬(u ∈ v)
8. l1 : A List
9. l2 : A List
10. bs = (l1 @ [u] @ l2) ∈ (A List)
11. (∀x∈v.(x ∈ bs))
12. sub-bag(A;v;l1 @ l2)
⊢ ↓sub-bag(A;[u / v];bs)
BY
{ ((HypSubst (-3) 0 THENA Auto)
   THEN D 0
   THEN All(Unfold `sub-bag`)
   THEN ExRepD
   THEN All(Fold `bag-append`)
   THEN (RWO "bag-append-comm-assoc" 0 THENA Auto)
   THEN (InstConcl [⌜cs⌝]⋅ THENA Auto)
   THEN (HypSubst (-1) 0 THENA Auto)
   THEN (RW (AddrC [2] (LemmaC `bag-append-comm`)) 0 THENA Auto)
   THEN RepUR ``bag-append`` 0
   THEN Folds ``bag-append cons-bag`` 0
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  A  :  Type
2.  u  :  A
3.  v  :  A  List
4.  \mforall{}bs:A  List.  (no\_repeats(A;v)  {}\mRightarrow{}  (\mforall{}x\mmember{}v.(x  \mmember{}  bs))  {}\mRightarrow{}  (\mdownarrow{}sub-bag(A;v;bs)))
5.  bs  :  A  List
6.  no\_repeats(A;v)
7.  \mneg{}(u  \mmember{}  v)
8.  l1  :  A  List
9.  l2  :  A  List
10.  bs  =  (l1  @  [u]  @  l2)
11.  (\mforall{}x\mmember{}v.(x  \mmember{}  bs))
12.  sub-bag(A;v;l1  @  l2)
\mvdash{}  \mdownarrow{}sub-bag(A;[u  /  v];bs)


By

---

Latex:
((HypSubst  (-3)  0  THENA  Auto)
  THEN  D  0
  THEN  All(Unfold  `sub-bag`)
  THEN  ExRepD
  THEN  All(Fold  `bag-append`)
  THEN  (RWO  "bag-append-comm-assoc"  0  THENA  Auto)
  THEN  (InstConcl  [\mkleeneopen{}cs\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst  (-1)  0  THENA  Auto)
  THEN  (RW  (AddrC  [2]  (LemmaC  `bag-append-comm`))  0  THENA  Auto)
  THEN  RepUR  ``bag-append``  0
  THEN  Folds  ``bag-append  cons-bag``  0
  THEN  Auto)\mcdot{}

---

Home Index