---

Step * of Lemma bag-append-is-single-iff2

∀[T:Type]. ∀[x:T].
  ∀as,bs:bag(T).
    uiff({x} = (as + bs) ∈ bag(T);↓((as = {x} ∈ bag(T)) ∧ (bs = {} ∈ bag(T)))
                                   ∨ ((bs = {x} ∈ bag(T)) ∧ (as = {} ∈ bag(T))))
BY
{ ((UnivCD THENA Auto)
   THEN D 0
   THEN Auto
   THEN Try (Complete ((RWO "bag-append-is-single-iff<" 0 THEN Auto)))
   THEN Try (Complete ((RWO "bag-append-is-single-iff<" (-1) THEN Auto)))) }

1
1. T : Type
2. x : T
3. as : bag(T)
4. bs : bag(T)
5. ((as = {x} ∈ bag(T)) ∧ (bs = {} ∈ bag(T))) ∨ ((bs = {x} ∈ bag(T)) ∧ (as = {} ∈ bag(T)))
⊢ {x} = (as + bs) ∈ bag(T)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[x:T].
    \mforall{}as,bs:bag(T).    uiff(\{x\}  =  (as  +  bs);\mdownarrow{}((as  =  \{x\})  \mwedge{}  (bs  =  \{\}))  \mvee{}  ((bs  =  \{x\})  \mwedge{}  (as  =  \{\})))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  Try  (Complete  ((RWO  "bag-append-is-single-iff<"  0  THEN  Auto)))
  THEN  Try  (Complete  ((RWO  "bag-append-is-single-iff<"  (-1)  THEN  Auto))))

---

Home Index