---

Step * 2 1 1 2 1 1 1 of Lemma sub-bag-iff


1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. num : T ⟶ ℕ
5. ∀x:T. ((num x) ≤ (#x in bs))
6. ∀x:T. ∀n:ℕ.  (repn(n;x) ∈ bag(T))
7. x : T
⊢ (#x in bag-union(bag-map(λx.repn(num x;x);bag-to-set(eq;bs)))) = (num x) ∈ ℤ
BY
{ ((InstLemma `member-bag-to-set` [⌜T⌝;⌜eq⌝;⌜bs⌝;⌜x⌝]⋅ THENA Auto)
   THEN (Assert (#x in bag-to-set(eq;bs)) = if 0 <z (#x in bs) then 1 else 0 fi  ∈ ℤ BY
               ((InstLemma `count-bag-to-set` [⌜T⌝;⌜eq⌝;⌜bs⌝;⌜x⌝]⋅ THENM HypSubst' -1 0) THEN Auto))
   ) }

1
1. T : Type
2. eq : EqDecider(T)
3. bs : bag(T)
4. num : T ⟶ ℕ
5. ∀x:T. ((num x) ≤ (#x in bs))
6. ∀x:T. ∀n:ℕ.  (repn(n;x) ∈ bag(T))
7. x : T
8. uiff(x ↓∈ bs;x ↓∈ bag-to-set(eq;bs))
9. (#x in bag-to-set(eq;bs)) = if 0 <z (#x in bs) then 1 else 0 fi  ∈ ℤ
⊢ (#x in bag-union(bag-map(λx.repn(num x;x);bag-to-set(eq;bs)))) = (num x) ∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  eq  :  EqDecider(T)
3.  bs  :  bag(T)
4.  num  :  T  {}\mrightarrow{}  \mBbbN{}
5.  \mforall{}x:T.  ((num  x)  \mleq{}  (\#x  in  bs))
6.  \mforall{}x:T.  \mforall{}n:\mBbbN{}.    (repn(n;x)  \mmember{}  bag(T))
7.  x  :  T
\mvdash{}  (\#x  in  bag-union(bag-map(\mlambda{}x.repn(num  x;x);bag-to-set(eq;bs))))  =  (num  x)


By

---

Latex:
((InstLemma  `member-bag-to-set`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  (\#x  in  bag-to-set(eq;bs))  =  if  0  <z  (\#x  in  bs)  then  1  else  0  fi    BY
                          ((InstLemma  `count-bag-to-set`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENM  HypSubst'  -1  0)  THEN  Auto))
  )

---

Home Index