---

Step * of Lemma bag-member-bag-diff

∀[T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀bs:bag(T).  uiff(x ↓∈ bs;↑isl(bag-diff(eq;bs;{x})))
BY
{ xxx((UnivCD THENA Auto)
      THEN ((RWO "bag-member-iff" 0 THENA Auto) THEN (InstLemma `bag-diff-property` [⌜T⌝;⌜eq⌝;⌜{x}⌝;⌜bs⌝]⋅ THENA Auto))
      THEN MoveToConcl (-1)
      THEN GenConclAtAddr [1;1]
      THEN D -2
      THEN Reduce 0
      THEN Auto)xxx }

1
1. T : Type
2. eq : EqDecider(T)
3. x : T
4. bs : bag(T)
5. y : Unit
6. bag-diff(eq;bs;{x}) = (inr y ) ∈ (bag(T)?)
7. ∀cs:bag(T). (¬(bs = ({x} + cs) ∈ bag(T)))
8. ∃as:bag(T). (bs = ({x} + as) ∈ bag(T))
⊢ False

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}eq:EqDecider(T).  \mforall{}x:T.  \mforall{}bs:bag(T).    uiff(x  \mdownarrow{}\mmember{}  bs;\muparrow{}isl(bag-diff(eq;bs;\{x\})))


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  ((RWO  "bag-member-iff"  0  THENA  Auto)
                    THEN  (InstLemma  `bag-diff-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}\{x\}\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}  THENA  Auto)
                    )
        THEN  MoveToConcl  (-1)
        THEN  GenConclAtAddr  [1;1]
        THEN  D  -2
        THEN  Reduce  0
        THEN  Auto)xxx

---

Home Index