---

Step * 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. v : bag(T)?
7. v1 : bag(T)?
⊢ ((∃as:bag(T). ((x = ({a} + as) ∈ bag(T)) ∧ (v1 = (inl as) ∈ (bag(T)?)))) ∨ ((¬a ↓∈ x) ∧ (v1 = (inr ⋅ ) ∈ (bag(T)?))))
⇒ ((∃as:bag(T). ((x = ({y} + as) ∈ bag(T)) ∧ (v = (inl as) ∈ (bag(T)?)))) ∨ ((¬y ↓∈ x) ∧ (v = (inr ⋅ ) ∈ (bag(T)?))))
⇒ (case v of inl(b) => bag-remove1(eq;b;a) | inr(z) => v
   = case v1 of inl(b) => bag-remove1(eq;b;y) | inr(z) => v1
   ∈ (bag(T)?))
BY
{ (Auto
   THEN SplitOrHyps
   THEN SquashExRepD
   THEN (AllHyps (ImpossibleEq Auto)⋅ THEN Auto)
   THEN AllHyps ReduceUnionEq ⋅
   THEN Auto) }

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

2
1. T : Type
2. eq : EqDecider(T)
3. x : bag(T)
4. a : T
5. y : T
6. x1 : bag(T)
7. y1 : Unit
8. ¬a ↓∈ x
9. y1 = ⋅ ∈ Unit
10. as : bag(T)
11. x = ({y} + as) ∈ bag(T)
12. x1 = as ∈ bag(T)
⊢ bag-remove1(eq;x1;a) = (inr y1 ) ∈ (bag(T)?)

3
1. T : Type
2. eq : EqDecider(T)
3. x : bag(T)
4. a : T
5. y : T
6. y1 : Unit
7. x1 : bag(T)
8. as : bag(T)
9. x = ({a} + as) ∈ bag(T)
10. x1 = as ∈ bag(T)
11. ¬y ↓∈ x
12. y1 = ⋅ ∈ Unit
⊢ (inr y1 ) = bag-remove1(eq;x1;y) ∈ (bag(T)?)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  x  :  bag(T)
4.  a  :  T
5.  y  :  T
6.  v  :  bag(T)?
7.  v1  :  bag(T)?
\mvdash{}  ((\mexists{}as:bag(T).  ((x  =  (\{a\}  +  as))  \mwedge{}  (v1  =  (inl  as))))  \mvee{}  ((\mneg{}a  \mdownarrow{}\mmember{}  x)  \mwedge{}  (v1  =  (inr  \mcdot{}  ))))
{}\mRightarrow{}  ((\mexists{}as:bag(T).  ((x  =  (\{y\}  +  as))  \mwedge{}  (v  =  (inl  as))))  \mvee{}  ((\mneg{}y  \mdownarrow{}\mmember{}  x)  \mwedge{}  (v  =  (inr  \mcdot{}  ))))
{}\mRightarrow{}  (case  v  of  inl(b)  =>  bag-remove1(eq;b;a)  |  inr(z)  =>  v
      =  case  v1  of  inl(b)  =>  bag-remove1(eq;b;y)  |  inr(z)  =>  v1)


By

---

Latex:
(Auto
  THEN  SplitOrHyps
  THEN  SquashExRepD
  THEN  (AllHyps  (ImpossibleEq  Auto)\mcdot{}  THEN  Auto)
  THEN  AllHyps  ReduceUnionEq  \mcdot{}
  THEN  Auto)

---

Home Index