---

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


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)
BY
{ ((InstLemma `bag-append-comm` [⌜T⌝;⌜[y∈as|¬b(eq x y)]⌝;⌜[a∈as|eqof(eq) a x]⌝]⋅ THENA Auto)
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN Thin (-1)
   THEN (InstLemma `bag-filter-split` [⌜T⌝;⌜λa.(eqof(eq) a x)⌝;⌜as⌝]⋅ THENA Auto)
   THEN RepUR ``so_apply`` (-1)
   THEN (Subst ⌜[x@0∈as|¬b(eqof(eq) x@0 x)] = [y∈as|¬b(eq x y)] ∈ bag(T)⌝ (-1)⋅ THENM (HypSubst' (-1) 0 THEN Auto))
   THEN Auto)⋅ }

1
.....equality..... 
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)
7. ([x@0∈as|eqof(eq) x@0 x] + [x@0∈as|¬b(eqof(eq) x@0 x)]) = as ∈ bag(T)
⊢ [x@0∈as|¬b(eqof(eq) x@0 x)] = [y∈as|¬b(eq x y)] ∈ bag(T)

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  as  :  bag(T)
4.  x  :  T
5.  cs  :  bag(T)
6.  \muparrow{}bag-deq-member(eq;x;as)
\mvdash{}  (as  +  cs)  =  (([y\mmember{}as|\mneg{}\msubb{}(eq  x  y)]  +  [a\mmember{}as|eqof(eq)  a  x])  +  cs)


By

---

Latex:
((InstLemma  `bag-append-comm`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}[y\mmember{}as|\mneg{}\msubb{}(eq  x  y)]\mkleeneclose{};\mkleeneopen{}[a\mmember{}as|eqof(eq)  a  x]\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  Thin  (-1)
  THEN  (InstLemma  `bag-filter-split`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}\mlambda{}a.(eqof(eq)  a  x)\mkleeneclose{};\mkleeneopen{}as\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RepUR  ``so\_apply``  (-1)
  THEN  (Subst  \mkleeneopen{}[x@0\mmember{}as|\mneg{}\msubb{}(eqof(eq)  x@0  x)]  =  [y\mmember{}as|\mneg{}\msubb{}(eq  x  y)]\mkleeneclose{}  (-1)\mcdot{}
  THENM  (HypSubst'  (-1)  0  THEN  Auto)
  )
  THEN  Auto)\mcdot{}

---

Home Index