---

Step * 1 of Lemma sub-bag-remove-if


1. [T] : Type
2. [bs] : bag(T)
3. eq : EqDecider(T)
4. as : bag(T)
5. x : T
6. cs : bag(T)
7. bs = (as + cs) ∈ bag(T)
8. ↑bag-deq-member(eq;x;as)
⊢ ∃cs:bag(T). (bs = (as - x + cs) ∈ bag(T))
BY
{ ((InstConcl [⌜cs + [a∈as|eqof(eq) a x]⌝]⋅ THENA Auto)
   THEN (HypSubst' (-2) 0 THENA Auto)
   THEN ThinVar `bs'
   THEN RepUR ``bag-remove`` 0
   THEN (InstLemma `bag-append-comm` [⌜T⌝;⌜cs⌝;⌜[a∈as|eqof(eq) a x]⌝]⋅ THENA Auto)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN Thin (-1)
   THEN (RWO "bag-append-assoc<" 0 THENA Auto)) }

1
1. T : Type
2. eq : EqDecider(T)
3. as : bag(T)
4. x : T
5. cs : bag(T)
6. ↑bag-deq-member(eq;x;as)
⊢ (as + cs) = (([y∈as|¬b(eq x y)] + [a∈as|eqof(eq) a x]) + cs) ∈ bag(T)

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [bs]  :  bag(T)
3.  eq  :  EqDecider(T)
4.  as  :  bag(T)
5.  x  :  T
6.  cs  :  bag(T)
7.  bs  =  (as  +  cs)
8.  \muparrow{}bag-deq-member(eq;x;as)
\mvdash{}  \mexists{}cs:bag(T).  (bs  =  (as  -  x  +  cs))


By

---

Latex:
((InstConcl  [\mkleeneopen{}cs  +  [a\mmember{}as|eqof(eq)  a  x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-2)  0  THENA  Auto)
  THEN  ThinVar  `bs'
  THEN  RepUR  ``bag-remove``  0
  THEN  (InstLemma  `bag-append-comm`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}cs\mkleeneclose{};\mkleeneopen{}[a\mmember{}as|eqof(eq)  a  x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (RWO  "bag-append-assoc<"  0  THENA  Auto))

---

Home Index