---

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

∀[A:Type]. ∀as:bag(A). ∀bs:A List.  (bag-no-repeats(A;as) ⇒ b_all(A;as;x.(x ∈ bs)) ⇒ (↓sub-bag(A;as;bs)))
BY
{ (Auto
   THEN (BagToList 2 THENA Auto)
   THEN (Assert ⌜no_repeats(A;as)⌝⋅
         THENA (D (-2)
                THEN (Unhide THENA Auto)
                THEN ExRepD
                THEN (Assert ⌜as = L ∈ bag(A)⌝⋅ THENA Auto)
                THEN FLemma `no_repeats-bag` [-1;-3]
                THEN Auto)
         )
   THEN Thin (-3)
   THEN (Assert ⌜(∀x∈as.(x ∈ bs))⌝⋅
         THENA ((RWO "l_all_iff" 0 THEN Auto)
                THEN UnfoldTopAb (-4)
                THEN BackThruSomeHyp
                THEN BLemma `list-member-bag-member`
                THEN Auto)
         )
   THEN Thin (-3)
   THEN RepeatFor 3 (MoveToConcl (-1))
   THEN ListInd (-1)
   THEN Auto
   THEN Try (Complete ((D 0 THEN Fold `empty-bag` 0 THEN BLemma `empty-sub-bag` THEN Auto)))
   THEN (All(RW ListC) THENA Auto)
   THEN RepD
   THEN (RWO "l_member_decomp" (-2) THENA Auto)
   THEN ExRepD
   THEN InstHyp [⌜l1 @ l2⌝] (-8)⋅
   THEN Auto) }

1
.....antecedent..... 
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))
⊢ (∀x∈v.(x ∈ l1 @ l2))

2
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)

---

Latex:

---

Latex:
\mforall{}[A:Type]
    \mforall{}as:bag(A).  \mforall{}bs:A  List.    (bag-no-repeats(A;as)  {}\mRightarrow{}  b\_all(A;as;x.(x  \mmember{}  bs))  {}\mRightarrow{}  (\mdownarrow{}sub-bag(A;as;bs)))


By

---

Latex:
(Auto
  THEN  (BagToList  2  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}no\_repeats(A;as)\mkleeneclose{}\mcdot{}
              THENA  (D  (-2)
                            THEN  (Unhide  THENA  Auto)
                            THEN  ExRepD
                            THEN  (Assert  \mkleeneopen{}as  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)
                            THEN  FLemma  `no\_repeats-bag`  [-1;-3]
                            THEN  Auto)
              )
  THEN  Thin  (-3)
  THEN  (Assert  \mkleeneopen{}(\mforall{}x\mmember{}as.(x  \mmember{}  bs))\mkleeneclose{}\mcdot{}
              THENA  ((RWO  "l\_all\_iff"  0  THEN  Auto)
                            THEN  UnfoldTopAb  (-4)
                            THEN  BackThruSomeHyp
                            THEN  BLemma  `list-member-bag-member`
                            THEN  Auto)
              )
  THEN  Thin  (-3)
  THEN  RepeatFor  3  (MoveToConcl  (-1))
  THEN  ListInd  (-1)
  THEN  Auto
  THEN  Try  (Complete  ((D  0  THEN  Fold  `empty-bag`  0  THEN  BLemma  `empty-sub-bag`  THEN  Auto)))
  THEN  (All(RW  ListC)  THENA  Auto)
  THEN  RepD
  THEN  (RWO  "l\_member\_decomp"  (-2)  THENA  Auto)
  THEN  ExRepD
  THEN  InstHyp  [\mkleeneopen{}l1  @  l2\mkleeneclose{}]  (-8)\mcdot{}
  THEN  Auto)

---

Home Index