---

Step * 2 1 of Lemma bag-append-is-single


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)
10. ((||v|| + ||[u1 / v1]||) + 1) = 1 ∈ ℤ
⊢ ↓(([u / v] = {x} ∈ bag(T)) ∧ ([u1 / v1] = {} ∈ bag(T))) ∨ (([u1 / v1] = {x} ∈ bag(T)) ∧ ([u / v] = {} ∈ bag(T)))
BY
{ (Reduce (-1) THEN Auto') }

---

Latex:

---

Latex:

1.  T  :  Type
2.  x  :  T
3.  u  :  T
4.  v  :  T  List
5.  u1  :  T
6.  v1  :  T  List
7.  (((v  +  v1)  =  \{x\})  {}\mRightarrow{}  (\mdownarrow{}((v  =  \{x\})  \mwedge{}  (v1  =  \{\}))  \mvee{}  ((v1  =  \{x\})  \mwedge{}  (v  =  \{\}))))
{}\mRightarrow{}  (([u  /  v]  +  v1)  =  \{x\})
{}\mRightarrow{}  (\mdownarrow{}(([u  /  v]  =  \{x\})  \mwedge{}  (v1  =  \{\}))  \mvee{}  ((v1  =  \{x\})  \mwedge{}  ([u  /  v]  =  \{\})))
8.  ((v  +  [u1  /  v1])  =  \{x\})  {}\mRightarrow{}  (\mdownarrow{}((v  =  \{x\})  \mwedge{}  ([u1  /  v1]  =  \{\}))  \mvee{}  (([u1  /  v1]  =  \{x\})  \mwedge{}  (v  =  \{\})))
9.  ([u  /  v]  +  [u1  /  v1])  =  \{x\}
10.  ((||v||  +  ||[u1  /  v1]||)  +  1)  =  1
\mvdash{}  \mdownarrow{}(([u  /  v]  =  \{x\})  \mwedge{}  ([u1  /  v1]  =  \{\}))  \mvee{}  (([u1  /  v1]  =  \{x\})  \mwedge{}  ([u  /  v]  =  \{\}))


By

---

Latex:
(Reduce  (-1)  THEN  Auto')

---

Home Index