---

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

∀[T:Type]. ∀[x:T].
  ∀as,bs:bag(T).
    uiff((as + bs) = {x} ∈ 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) }

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

2
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)))
⊢ (as + bs) = {x} ∈ bag(T)

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  D  0  THEN  Auto)

---

Home Index