---

Step * 2 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)
⊢ ↓(([u / v] = {x} ∈ bag(T)) ∧ ([u1 / v1] = {} ∈ bag(T))) ∨ (([u1 / v1] = {x} ∈ bag(T)) ∧ ([u / v] = {} ∈ bag(T)))
BY
{ ((Assert #([u / v] + [u1 / v1]) = #({x}) ∈ ℤ BY
          Auto)
   THEN RepUR ``bag-size bag-append single-bag`` -1
   THEN RWO "length-append" (-1)
   THEN Auto) }

1
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)))

---

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\}
\mvdash{}  \mdownarrow{}(([u  /  v]  =  \{x\})  \mwedge{}  ([u1  /  v1]  =  \{\}))  \mvee{}  (([u1  /  v1]  =  \{x\})  \mwedge{}  ([u  /  v]  =  \{\}))


By

---

Latex:
((Assert  \#([u  /  v]  +  [u1  /  v1])  =  \#(\{x\})  BY
                Auto)
  THEN  RepUR  ``bag-size  bag-append  single-bag``  -1
  THEN  RWO  "length-append"  (-1)
  THEN  Auto)

---

Home Index