---

Step * 1 of Lemma sub-bag-no-repeats-iff


1. [T] : Type
2. eq : EqDecider(T)
3. b1 : bag(T)
4. b2 : bag(T)
5. bag-no-repeats(T;b1)
6. ∀x:T. (x ↓∈ b1 ⇒ x ↓∈ b2)
⊢ sub-bag(T;b1;b2)
BY
{ ((InstLemma `sub-bag-iff` [⌜T⌝;⌜eq⌝;⌜b1⌝;⌜b2⌝]⋅ THENA Auto)
   THEN RWO "-1" 0
   THEN Auto
   THEN (Assert ⌜((#x in b1) = 0 ∈ ℤ) ∨ (1 ≤ (#x in b1))⌝⋅ THENA (Auto THEN Decide ⌜(#x in b1) = 0 ∈ ℤ⌝⋅ THEN Auto'))
   THEN (D (-1)
         THEN Try (Complete ((HypSubst' (-1) 0 THEN Auto)))
         THEN (InstLemma `bag-no-repeats-count` [⌜T⌝;⌜eq⌝;⌜b1⌝]⋅ THENA Auto)
         THEN D (-1)
         THEN Thin (-1)
         THEN (D (-1) THENA Auto)
         THEN (InstHyp [⌜x⌝] (-1)⋅ THENA Auto)
         THEN Thin (-2)
         THEN (RWO "-1" (-2) THENA Auto)
         THEN Thin (-1)
         THEN HypSubst' (-1) 0
         THEN (Assert ⌜1 ≤ (#x in b1)⌝⋅ THENA Auto)
         THEN (RWO "bag-count-member" (-1) THENA Auto)
         THEN (InstHyp [⌜x⌝] (-6)⋅ THENA Auto)
         THEN RWO "bag-count-member" 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  eq  :  EqDecider(T)
3.  b1  :  bag(T)
4.  b2  :  bag(T)
5.  bag-no-repeats(T;b1)
6.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b1  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  b2)
\mvdash{}  sub-bag(T;b1;b2)


By

---

Latex:
((InstLemma  `sub-bag-iff`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{};\mkleeneopen{}b2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO  "-1"  0
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}((\#x  in  b1)  =  0)  \mvee{}  (1  \mleq{}  (\#x  in  b1))\mkleeneclose{}\mcdot{}
              THENA  (Auto  THEN  Decide  \mkleeneopen{}(\#x  in  b1)  =  0\mkleeneclose{}\mcdot{}  THEN  Auto')
              )
  THEN  (D  (-1)
              THEN  Try  (Complete  ((HypSubst'  (-1)  0  THEN  Auto)))
              THEN  (InstLemma  `bag-no-repeats-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}b1\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  D  (-1)
              THEN  Thin  (-1)
              THEN  (D  (-1)  THENA  Auto)
              THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
              THEN  Thin  (-2)
              THEN  (RWO  "-1"  (-2)  THENA  Auto)
              THEN  Thin  (-1)
              THEN  HypSubst'  (-1)  0
              THEN  (Assert  \mkleeneopen{}1  \mleq{}  (\#x  in  b1)\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  (RWO  "bag-count-member"  (-1)  THENA  Auto)
              THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-6)\mcdot{}  THENA  Auto)
              THEN  RWO  "bag-count-member"  0
              THEN  Auto)\mcdot{})

---

Home Index