---

Step * 1 of Lemma bag-summation-equal-implies-all-equal-1


1. Assoc(ℤ;λx,y. (x + y))
2. Comm(ℤ;λx,y. (x + y))
3. T : Type
4. b : T List
5. f : T ⟶ ℤ
6. g : T ⟶ ℤ
7. ∀x:T. (x ↓∈ b ⇒ (f[x] ≤ g[x]))
8. Σ(x∈b). g[x] ≤ Σ(x∈b). f[x]
9. x : T
10. x ↓∈ b
⊢ f[x] = g[x] ∈ ℤ
BY
{ (ListInd 4
   THEN Folds ``empty-bag cons-bag`` 0
   THEN Auto
   THEN Try (BagMemberD (-1))
   THEN RepUR ``bag-summation empty-bag bag-accum`` 0
   THEN Auto) }

1
1. Assoc(ℤ;λx,y. (x + y))
2. Comm(ℤ;λx,y. (x + y))
3. T : Type
4. f : T ⟶ ℤ
5. g : T ⟶ ℤ
6. x : T
7. u : T
8. v : T List
9. (∀x:T. (x ↓∈ v ⇒ (f[x] ≤ g[x]))) ⇒ (Σ(x∈v). g[x] ≤ Σ(x∈v). f[x]) ⇒ x ↓∈ v ⇒ (f[x] = g[x] ∈ ℤ)
10. ∀x:T. (x ↓∈ u.v ⇒ (f[x] ≤ g[x]))
11. Σ(x∈u.v). g[x] ≤ Σ(x∈u.v). f[x]
12. (x = u ∈ T) ↓∨ x ↓∈ v
⊢ f[x] = g[x] ∈ ℤ

---

Latex:

---

Latex:

1.  Assoc(\mBbbZ{};\mlambda{}x,y.  (x  +  y))
2.  Comm(\mBbbZ{};\mlambda{}x,y.  (x  +  y))
3.  T  :  Type
4.  b  :  T  List
5.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
6.  g  :  T  {}\mrightarrow{}  \mBbbZ{}
7.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (f[x]  \mleq{}  g[x]))
8.  \mSigma{}(x\mmember{}b).  g[x]  \mleq{}  \mSigma{}(x\mmember{}b).  f[x]
9.  x  :  T
10.  x  \mdownarrow{}\mmember{}  b
\mvdash{}  f[x]  =  g[x]


By

---

Latex:
(ListInd  4
  THEN  Folds  ``empty-bag  cons-bag``  0
  THEN  Auto
  THEN  Try  (BagMemberD  (-1))
  THEN  RepUR  ``bag-summation  empty-bag  bag-accum``  0
  THEN  Auto)

---

Home Index