---

Step * 1 of Lemma bag-summation_functionality_wrt_le_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. (f[x] ≤ g[x])
⊢ accumulate (with value c and list item x):
   f[x] + c
  over list:
    b
  with starting value:
   0) ≤ accumulate (with value c and list item x):
         g[x] + c
        over list:
          b
        with starting value:
         0)
BY
{ ((Assert ⌜∀x,y:ℤ.
              ((x ≤ y)
              ⇒ (accumulate (with value c and list item x):
                   f[x] + c
                  over list:
                    b
                  with starting value:
                   x) ≤ accumulate (with value c and list item x):
                         g[x] + c
                        over list:
                          b
                        with starting value:
                         y)))⌝⋅
   THENM (BHyp -1  THEN Auto)
   )
   THEN ListInd 4
   THEN Reduce 0
   THEN Auto
   THEN BackThruSomeHyp
   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. (f[x] ≤ g[x])
7. u : T
8. v : T List
9. ∀x,y:ℤ.
     ((x ≤ y)
     ⇒ (accumulate (with value c and list item x):
          f[x] + c
         over list:
           v
         with starting value:
          x) ≤ accumulate (with value c and list item x):
                g[x] + c
               over list:
                 v
               with starting value:
                y)))
10. x : ℤ
11. y : ℤ
12. x ≤ y
⊢ (f[u] + x) ≤ (g[u] + y)

---

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.  (f[x]  \mleq{}  g[x])
\mvdash{}  accumulate  (with  value  c  and  list  item  x):
      f[x]  +  c
    over  list:
        b
    with  starting  value:
      0)  \mleq{}  accumulate  (with  value  c  and  list  item  x):
                  g[x]  +  c
                over  list:
                    b
                with  starting  value:
                  0)


By

---

Latex:
((Assert  \mkleeneopen{}\mforall{}x,y:\mBbbZ{}.
                        ((x  \mleq{}  y)
                        {}\mRightarrow{}  (accumulate  (with  value  c  and  list  item  x):
                                  f[x]  +  c
                                over  list:
                                    b
                                with  starting  value:
                                  x)  \mleq{}  accumulate  (with  value  c  and  list  item  x):
                                              g[x]  +  c
                                            over  list:
                                                b
                                            with  starting  value:
                                              y)))\mkleeneclose{}\mcdot{}
  THENM  (BHyp  -1    THEN  Auto)
  )
  THEN  ListInd  4
  THEN  Reduce  0
  THEN  Auto
  THEN  BackThruSomeHyp
  THEN  Auto)

---

Home Index