---

Step * 1 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. 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] ∈ ℤ
BY
{ ((Assert IsMonoid(ℤ;λx,y. (x + y);0) BY
          RepeatFor 2 (((D 0 THEN Reduce 0) THEN Auto)))
   THEN ((RWO "bag-summation-cons" (-3) THENM Reduce (-3)) THENA 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. (g[u] + Σ(x∈v). g[x]) ≤ (f[u] + Σ(x∈v). f[x])
12. (x = u ∈ T) ↓∨ x ↓∈ v
13. IsMonoid(ℤ;λx,y. (x + y);0)
⊢ 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.  f  :  T  {}\mrightarrow{}  \mBbbZ{}
5.  g  :  T  {}\mrightarrow{}  \mBbbZ{}
6.  x  :  T
7.  u  :  T
8.  v  :  T  List
9.  (\mforall{}x:T.  (x  \mdownarrow{}\mmember{}  v  {}\mRightarrow{}  (f[x]  \mleq{}  g[x])))  {}\mRightarrow{}  (\mSigma{}(x\mmember{}v).  g[x]  \mleq{}  \mSigma{}(x\mmember{}v).  f[x])  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  v  {}\mRightarrow{}  (f[x]  =  g[x])
10.  \mforall{}x:T.  (x  \mdownarrow{}\mmember{}  u.v  {}\mRightarrow{}  (f[x]  \mleq{}  g[x]))
11.  \mSigma{}(x\mmember{}u.v).  g[x]  \mleq{}  \mSigma{}(x\mmember{}u.v).  f[x]
12.  (x  =  u)  \mdownarrow{}\mvee{}  x  \mdownarrow{}\mmember{}  v
\mvdash{}  f[x]  =  g[x]


By

---

Latex:
((Assert  IsMonoid(\mBbbZ{};\mlambda{}x,y.  (x  +  y);0)  BY
                RepeatFor  2  (((D  0  THEN  Reduce  0)  THEN  Auto)))
  THEN  ((RWO  "bag-summation-cons"  (-3)  THENM  Reduce  (-3))  THENA  Auto)
  )

---

Home Index