---

Step * of Lemma bag-drop-property

∀[T:Type]
  ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).
    ((bs = ({x} + bag-drop(eq;bs;x)) ∈ bag(T)) ∨ ((¬x ↓∈ bs) ∧ (bs = bag-drop(eq;bs;x) ∈ bag(T))))
BY
{ TACTIC:(InstLemma `bag-remove1-property` []
          THEN RepeatFor 4 (ParallelLast')
          THEN Unfold `bag-drop` 0
          THEN MoveToConcl (-1)
          THEN GenConclTerm ⌜bag-remove1(eq;bs;x)⌝⋅
          THEN Auto
          THEN ParallelLast
          THEN (D (-3) THEN ExRepD THEN All Reduce THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}bs:bag(T).
        ((bs  =  (\{x\}  +  bag-drop(eq;bs;x)))  \mvee{}  ((\mneg{}x  \mdownarrow{}\mmember{}  bs)  \mwedge{}  (bs  =  bag-drop(eq;bs;x))))


By

---

Latex:
TACTIC:(InstLemma  `bag-remove1-property`  []
                THEN  RepeatFor  4  (ParallelLast')
                THEN  Unfold  `bag-drop`  0
                THEN  MoveToConcl  (-1)
                THEN  GenConclTerm  \mkleeneopen{}bag-remove1(eq;bs;x)\mkleeneclose{}\mcdot{}
                THEN  Auto
                THEN  ParallelLast
                THEN  (D  (-3)  THEN  ExRepD  THEN  All  Reduce  THEN  Auto)\mcdot{})

---

Home Index