---

Step * of Lemma bag-append-is-single

∀[T:Type]. ∀[x:T].
  ∀as,bs:bag(T).
    ↓((as = {x} ∈ bag(T)) ∧ (bs = {} ∈ bag(T))) ∨ ((bs = {x} ∈ bag(T)) ∧ (as = {} ∈ bag(T))) 
    supposing (as + bs) = {x} ∈ bag(T)
BY
{ (Auto THEN RepeatFor 2 ((BagInd 3 THEN Auto))) }

1
1. T : Type
2. x : T
3. u : T
4. v : T List
5. ((v + []) = {x} ∈ bag(T)) ⇒ (↓((v = {x} ∈ bag(T)) ∧ ([] = {} ∈ bag(T))) ∨ (([] = {x} ∈ bag(T)) ∧ (v = {} ∈ bag(T))))
6. ([u / v] + []) = {x} ∈ bag(T)
⊢ ↓(([u / v] = {x} ∈ bag(T)) ∧ ([] = {} ∈ bag(T))) ∨ (([] = {x} ∈ bag(T)) ∧ ([u / v] = {} ∈ bag(T)))

2
1. T : Type
2. x : T
3. u : T
4. v : T List
5. u1 : T
6. v1 : T List
7. (((v + v1) = {x} ∈ bag(T))
   ⇒ (↓((v = {x} ∈ bag(T)) ∧ (v1 = {} ∈ bag(T))) ∨ ((v1 = {x} ∈ bag(T)) ∧ (v = {} ∈ bag(T)))))
⇒ (([u / v] + v1) = {x} ∈ bag(T))
⇒ (↓(([u / v] = {x} ∈ bag(T)) ∧ (v1 = {} ∈ bag(T))) ∨ ((v1 = {x} ∈ bag(T)) ∧ ([u / v] = {} ∈ bag(T))))
8. ((v + [u1 / v1]) = {x} ∈ bag(T))
⇒ (↓((v = {x} ∈ bag(T)) ∧ ([u1 / v1] = {} ∈ bag(T))) ∨ (([u1 / v1] = {x} ∈ bag(T)) ∧ (v = {} ∈ bag(T))))
9. ([u / v] + [u1 / v1]) = {x} ∈ bag(T)
⊢ ↓(([u / v] = {x} ∈ bag(T)) ∧ ([u1 / v1] = {} ∈ bag(T))) ∨ (([u1 / v1] = {x} ∈ bag(T)) ∧ ([u / v] = {} ∈ bag(T)))

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RepeatFor  2  ((BagInd  3  THEN  Auto)))

---

Home Index