---

Step * of Lemma bag-subtract-append

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:bag(T)].  (bag-subtract(eq;as + bs;as) = bs ∈ bag(T))
BY
{ xxx(Auto
      THEN (BagToList 3 THEN Auto)
      THEN (BagToList 4 THEN Auto)
      THEN MoveToConcl (-1)
      THEN ListInd (-1)
      THEN ((RepUR ``bag-subtract`` 0 THEN Auto)
            THEN Unfold `bag-accum` 0
            THEN Reduce 0
            THEN Fold `bag-accum` 0
            THEN Fold `bag-subtract` 0
            THEN Subst ⌜bag-drop(eq;[u / v] + bs;u) ~ v + bs⌝ 0⋅
            THEN Auto
            THEN RepUR ``bag-append`` 0
            THEN BLemma `bag-drop-head`
            THEN Auto)⋅)xxx }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[as,bs:bag(T)].    (bag-subtract(eq;as  +  bs;as)  =  bs)


By

---

Latex:
xxx(Auto
        THEN  (BagToList  3  THEN  Auto)
        THEN  (BagToList  4  THEN  Auto)
        THEN  MoveToConcl  (-1)
        THEN  ListInd  (-1)
        THEN  ((RepUR  ``bag-subtract``  0  THEN  Auto)
                    THEN  Unfold  `bag-accum`  0
                    THEN  Reduce  0
                    THEN  Fold  `bag-accum`  0
                    THEN  Fold  `bag-subtract`  0
                    THEN  Subst  \mkleeneopen{}bag-drop(eq;[u  /  v]  +  bs;u)  \msim{}  v  +  bs\mkleeneclose{}  0\mcdot{}
                    THEN  Auto
                    THEN  RepUR  ``bag-append``  0
                    THEN  BLemma  `bag-drop-head`
                    THEN  Auto)\mcdot{})xxx

---

Home Index