---

Step * of Lemma bag-sum_wf_nat

∀[A:Type]. ∀[f:A ⟶ ℕ]. ∀[ba:bag(A)].  (bag-sum(ba;x.f[x]) ∈ ℕ)
BY
{ (Auto
   THEN Assert ⌜↓0 ≤ bag-sum(ba;x.f[x])⌝⋅
   THEN Try ((D (-1) THEN Unhide THEN Auto))
   THEN UseWitness ⌜Ax⌝⋅
   THEN BagD (-1)
   THEN Auto
   THEN MemTypeCD) }

1
1. A : Type
2. f : A ⟶ ℕ
3. as : A List
4. bs : A List
5. permutation(A;as;bs)
⊢ 0 ≤ bag-sum(as;x.f[x])

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[ba:bag(A)].    (bag-sum(ba;x.f[x])  \mmember{}  \mBbbN{})


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}\mdownarrow{}0  \mleq{}  bag-sum(ba;x.f[x])\mkleeneclose{}\mcdot{}
  THEN  Try  ((D  (-1)  THEN  Unhide  THEN  Auto))
  THEN  UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}
  THEN  BagD  (-1)
  THEN  Auto
  THEN  MemTypeCD)

---

Home Index