---

Step * 1 of Lemma bag-sum_wf_nat


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])
BY
{ (ThinVar `bs'⋅ THEN RepUR ``bag-sum`` 0 THEN MoveToConcl (-1) THEN InductionOnLast THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  f  :  A  {}\mrightarrow{}  \mBbbN{}
3.  as  :  A  List
4.  bs  :  A  List
5.  permutation(A;as;bs)
\mvdash{}  0  \mleq{}  bag-sum(as;x.f[x])


By

---

Latex:
(ThinVar  `bs'\mcdot{}
  THEN  RepUR  ``bag-sum``  0
  THEN  MoveToConcl  (-1)
  THEN  InductionOnLast
  THEN  Reduce  0
  THEN  Auto)

---

Home Index