---

Step * of Lemma sub-bag-filter2

∀T:Type. ∀p1,p2:T ⟶ 𝔹. ∀b,c:bag(T).
  (sub-bag(T;b;[x∈c|p1[x]]) ⇒ sub-bag(T;b;[x∈c|p2[x]]) ⇒ sub-bag(T;b;[x∈c|p1[x] ∧b p2[x]]))
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "sub-bag-filter" (-2) THENA Auto)
   THEN (RWO "sub-bag-filter" (-1) THENA Auto)
   THEN (RWO "sub-bag-filter" 0 THENA Auto)
   THEN Auto
   THEN (InstHyp [⌜x⌝] (-5)⋅ THENA Auto)
   THEN (InstHyp [⌜x⌝] (-4)⋅ THENA Auto)
   THEN RWO "assert_of_band" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}p1,p2:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}b,c:bag(T).
    (sub-bag(T;b;[x\mmember{}c|p1[x]])  {}\mRightarrow{}  sub-bag(T;b;[x\mmember{}c|p2[x]])  {}\mRightarrow{}  sub-bag(T;b;[x\mmember{}c|p1[x]  \mwedge{}\msubb{}  p2[x]]))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "sub-bag-filter"  (-2)  THENA  Auto)
  THEN  (RWO  "sub-bag-filter"  (-1)  THENA  Auto)
  THEN  (RWO  "sub-bag-filter"  0  THENA  Auto)
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{}]  (-4)\mcdot{}  THENA  Auto)
  THEN  RWO  "assert\_of\_band"  0
  THEN  Auto)

---

Home Index