---

Step * of Lemma list_accum-triangle-inequality

∀[T:Type]. ∀[L:T List]. ∀[x,y:ℤ]. ∀[f,g:T ⟶ ℤ].
  (|accumulate (with value s and list item a):
     s + f[a]
    over list:
      L
    with starting value:
     x) - accumulate (with value s and list item a):
           s + g[a]
          over list:
            L
          with starting value:
           y)| ≤ accumulate (with value s and list item a):
                  s + |f[a] - g[a]|
                 over list:
                   L
                 with starting value:
                  |x - y|))
BY
{ (InductionOnList
   THEN Reduce 0
   THEN Auto
   THEN (RWO "4" 0 THENA Auto)
   THEN (Assert ∀[L:T List]. ∀[x,y:ℤ].
                  ((x ≤ y)
                  ⇒ (∀[f:T ⟶ ℤ]
                        (accumulate (with value s and list item a):
                          s + f[a]
                         over list:
                           L
                         with starting value:
                          x) ≤ accumulate (with value s and list item a):
                                s + f[a]
                               over list:
                                 L
                               with starting value:
                                y)))) BY
               (All Thin THEN InductionOnList THEN Reduce 0 THEN Auto))
   THEN BHyp (-1)
   THEN Auto
   THEN RWO "int-triangle-inequality<" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[x,y:\mBbbZ{}].  \mforall{}[f,g:T  {}\mrightarrow{}  \mBbbZ{}].
    (|accumulate  (with  value  s  and  list  item  a):
          s  +  f[a]
        over  list:
            L
        with  starting  value:
          x)  -  accumulate  (with  value  s  and  list  item  a):
                      s  +  g[a]
                    over  list:
                        L
                    with  starting  value:
                      y)|  \mleq{}  accumulate  (with  value  s  and  list  item  a):
                                    s  +  |f[a]  -  g[a]|
                                  over  list:
                                      L
                                  with  starting  value:
                                    |x  -  y|))


By

---

Latex:
(InductionOnList
  THEN  Reduce  0
  THEN  Auto
  THEN  (RWO  "4"  0  THENA  Auto)
  THEN  (Assert  \mforall{}[L:T  List].  \mforall{}[x,y:\mBbbZ{}].
                                ((x  \mleq{}  y)
                                {}\mRightarrow{}  (\mforall{}[f:T  {}\mrightarrow{}  \mBbbZ{}]
                                            (accumulate  (with  value  s  and  list  item  a):
                                                s  +  f[a]
                                              over  list:
                                                  L
                                              with  starting  value:
                                                x)  \mleq{}  accumulate  (with  value  s  and  list  item  a):
                                                            s  +  f[a]
                                                          over  list:
                                                              L
                                                          with  starting  value:
                                                            y))))  BY
                          (All  Thin  THEN  InductionOnList  THEN  Reduce  0  THEN  Auto))
  THEN  BHyp  (-1)
  THEN  Auto
  THEN  RWO  "int-triangle-inequality<"  0
  THEN  Auto)

---

Home Index