---

Step * 1 of Lemma bag-diff_wf


1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. as : bag(T)
5. x : bag(T)
6. a : T
7. y : T
⊢ case bag-remove1(eq;x;y)
 of inl(b) =>
 bag-remove1(eq;b;a)
 | inr(z) =>
 case inl x of inl(b) => bag-remove1(eq;b;y) | inr(z) => inl x
= case case inl x of inl(b) => bag-remove1(eq;b;a) | inr(z) => inl x
   of inl(b) =>
   bag-remove1(eq;b;y)
   | inr(z) =>
   case inl x of inl(b) => bag-remove1(eq;b;a) | inr(z) => inl x
∈ (bag(T)?)
BY
{ (Reduce 0
   THEN (InstLemma `bag-remove1-property` [⌜T⌝;⌜eq⌝;⌜a⌝;⌜x⌝]⋅ THENA Auto)
   THEN (InstLemma `bag-remove1-property` [⌜T⌝;⌜eq⌝;⌜y⌝;⌜x⌝]⋅ THENA Auto)
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN GenConclAtAddr [2;2;2;1]
   THEN GenConclAtAddr [2;2;3;1]
   THEN All Thin) }

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

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  bs  :  bag(T)
4.  as  :  bag(T)
5.  x  :  bag(T)
6.  a  :  T
7.  y  :  T
\mvdash{}  case  bag-remove1(eq;x;y)
  of  inl(b)  =>
  bag-remove1(eq;b;a)
  |  inr(z)  =>
  case  inl  x  of  inl(b)  =>  bag-remove1(eq;b;y)  |  inr(z)  =>  inl  x
=  case  case  inl  x  of  inl(b)  =>  bag-remove1(eq;b;a)  |  inr(z)  =>  inl  x
      of  inl(b)  =>
      bag-remove1(eq;b;y)
      |  inr(z)  =>
      case  inl  x  of  inl(b)  =>  bag-remove1(eq;b;a)  |  inr(z)  =>  inl  x


By

---

Latex:
(Reduce  0
  THEN  (InstLemma  `bag-remove1-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `bag-remove1-property`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  GenConclAtAddr  [2;2;2;1]
  THEN  GenConclAtAddr  [2;2;3;1]
  THEN  All  Thin)

---

Home Index