---

Step * 1 1 1 of Lemma bag-diff_wf


1. T : Type
2. eq : EqDecider(T)
3. x : bag(T)
4. a : T
5. y : T
6. x1 : bag(T)
7. x2 : bag(T)
8. a1 : bag(T)
9. x = ({a} + a1) ∈ bag(T)
10. x2 = a1 ∈ bag(T)
11. as : bag(T)
12. x = ({y} + as) ∈ bag(T)
13. x1 = as ∈ bag(T)
⊢ bag-remove1(eq;x1;a) = bag-remove1(eq;x2;y) ∈ (bag(T)?)
BY
{ (RWO  "bag-remove1-equal" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  bag(T)
4.  a  :  T
5.  y  :  T
6.  x1  :  bag(T)
7.  x2  :  bag(T)
8.  a1  :  bag(T)
9.  x  =  (\{a\}  +  a1)
10.  x2  =  a1
11.  as  :  bag(T)
12.  x  =  (\{y\}  +  as)
13.  x1  =  as
\mvdash{}  bag-remove1(eq;x1;a)  =  bag-remove1(eq;x2;y)


By

---

Latex:
(RWO    "bag-remove1-equal"  0  THEN  Auto)

---

Home Index