---

Step * 3 of Lemma sub-bag-filter


1. [T] : Type
2. p : T ⟶ 𝔹
3. b : bag(T)
4. c : bag(T)
5. sub-bag(T;b;c)
6. ∀x:T. (x ↓∈ b ⇒ (↑p[x]))
⊢ sub-bag(T;b;[x∈c|p[x]])
BY
{ (All (Unfold `sub-bag`)⋅
   THEN ExRepD
   THEN (Assert ⌜[x∈c|p[x]] = [x∈b + cs|p[x]] ∈ bag(T)⌝⋅ THENA (HypSubst' (-2) 0 THEN Auto THEN DoSubsume THEN Auto))
   THEN (RWO "bag-filter-append" (-1) THENA Auto)
   THEN (HypSubst' (-1) 0 THEN Auto)
   THEN (InstConcl [⌜[x∈cs|p[x]]⌝]⋅ THENA Auto)⋅
   THEN (Assert ⌜[x∈b|p[x]] = b ∈ bag(T)⌝⋅ THENA (RWO "bag-filter-trivial2" 0 THEN Auto))
   THEN HypSubst' (-1) 0⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  p  :  T  {}\mrightarrow{}  \mBbbB{}
3.  b  :  bag(T)
4.  c  :  bag(T)
5.  sub-bag(T;b;c)
6.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\muparrow{}p[x]))
\mvdash{}  sub-bag(T;b;[x\mmember{}c|p[x]])


By

---

Latex:
(All  (Unfold  `sub-bag`)\mcdot{}
  THEN  ExRepD
  THEN  (Assert  \mkleeneopen{}[x\mmember{}c|p[x]]  =  [x\mmember{}b  +  cs|p[x]]\mkleeneclose{}\mcdot{}
              THENA  (HypSubst'  (-2)  0  THEN  Auto  THEN  DoSubsume  THEN  Auto)
              )
  THEN  (RWO  "bag-filter-append"  (-1)  THENA  Auto)
  THEN  (HypSubst'  (-1)  0  THEN  Auto)
  THEN  (InstConcl  [\mkleeneopen{}[x\mmember{}cs|p[x]]\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}
  THEN  (Assert  \mkleeneopen{}[x\mmember{}b|p[x]]  =  b\mkleeneclose{}\mcdot{}  THENA  (RWO  "bag-filter-trivial2"  0  THEN  Auto))
  THEN  HypSubst'  (-1)  0\mcdot{}
  THEN  Auto)

---

Home Index