---

Step * 2 1 1 2 1 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
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) ∈ ℤ
BY
{ (RepeatFor 2 (MoveToConcl (-1)) THEN GenConclAtAddr [1;2;3] THEN Thin (-1) 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. v : bag(T)
9. x ↓∈ v supposing x ↓∈ bs
10. x ↓∈ bs supposing x ↓∈ v
11. (#x in v) = if 0 <z (#x in bs) then 1 else 0 fi  ∈ ℤ
⊢ (#x in bag-union(bag-map(λx.repn(num x;x);v))) = (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
8.  uiff(x  \mdownarrow{}\mmember{}  bs;x  \mdownarrow{}\mmember{}  bag-to-set(eq;bs))
9.  (\#x  in  bag-to-set(eq;bs))  =  if  0  <z  (\#x  in  bs)  then  1  else  0  fi 
\mvdash{}  (\#x  in  bag-union(bag-map(\mlambda{}x.repn(num  x;x);bag-to-set(eq;bs))))  =  (num  x)


By

---

Latex:
(RepeatFor  2  (MoveToConcl  (-1))  THEN  GenConclAtAddr  [1;2;3]  THEN  Thin  (-1)  THEN  Auto)

---

Home Index