---

Step * of Lemma sub-bag-equal

∀[T:Type]. ∀[b1,b2:bag(T)].  (b1 = b2 ∈ bag(T)) supposing (sub-bag(T;b1;b2) and sub-bag(T;b2;b1))
BY
{ ((UnivCD THENA Auto)
   THEN All (RepUR ``sub-bag``)
   THEN ExRepD
   THEN (HypSubst' (-3) (-1) THENA Auto)
   THEN ((RWO "bag-append-assoc" (-1) THENA Auto)
         THEN (InstLemma `bag-append-empty` [⌜b2⌝]⋅ THENA Auto)
         THEN (Assert ⌜(b2 + {}) = (b2 + c1 + cs) ∈ bag(T)⌝⋅ THENA (HypSubst' (-1) 0 THEN Auto))
         THEN RWO "bag-append-cancel" (-1)
         THEN Auto
         THEN InstLemma `bag-append-eq-empty` [⌜T⌝;⌜c1⌝;⌜cs⌝]⋅
         THEN Auto
         THEN D -2
         THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[b1,b2:bag(T)].    (b1  =  b2)  supposing  (sub-bag(T;b1;b2)  and  sub-bag(T;b2;b1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  All  (RepUR  ``sub-bag``)
  THEN  ExRepD
  THEN  (HypSubst'  (-3)  (-1)  THENA  Auto)
  THEN  ((RWO  "bag-append-assoc"  (-1)  THENA  Auto)
              THEN  (InstLemma  `bag-append-empty`  [\mkleeneopen{}b2\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (Assert  \mkleeneopen{}(b2  +  \{\})  =  (b2  +  c1  +  cs)\mkleeneclose{}\mcdot{}  THENA  (HypSubst'  (-1)  0  THEN  Auto))
              THEN  RWO  "bag-append-cancel"  (-1)
              THEN  Auto
              THEN  InstLemma  `bag-append-eq-empty`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}c1\mkleeneclose{};\mkleeneopen{}cs\mkleeneclose{}]\mcdot{}
              THEN  Auto
              THEN  D  -2
              THEN  Auto)\mcdot{})

---

Home Index