---

Step * 2 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⌝]⋅ THEN Auto)
   THEN (HypSubst' (-2) 0 THENA Auto)
   THEN ThinVar `bs'
   THEN RepUR ``bag-remove`` 0
   THEN (RWO "bag-filter-trivial2" 0
         THEN Auto
         THEN (RW assert_pushdownC (-3) THENA Auto)
         THEN (RW assert_pushdownC 0 THENA Auto)
         THEN ParallelOp (-3)
         THEN Auto)⋅) }

---

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.  \mneg{}\muparrow{}bag-deq-member(eq;x;as)
\mvdash{}  \mexists{}cs:bag(T).  (bs  =  (as  -  x  +  cs))


By

---

Latex:
((InstConcl  [\mkleeneopen{}cs\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (HypSubst'  (-2)  0  THENA  Auto)
  THEN  ThinVar  `bs'
  THEN  RepUR  ``bag-remove``  0
  THEN  (RWO  "bag-filter-trivial2"  0
              THEN  Auto
              THEN  (RW  assert\_pushdownC  (-3)  THENA  Auto)
              THEN  (RW  assert\_pushdownC  0  THENA  Auto)
              THEN  ParallelOp  (-3)
              THEN  Auto)\mcdot{})

---

Home Index