Nuprl 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|))


Proof



Definitions occuring in Statement :  list_accum: list_accum,  list: T List,  absval: |i|,  uall: ∀[x:A]. B[x],  so_apply: x[s],  le: A ≤ B,  function: x:A ⟶ B[x],  subtract: n - m,  add: n + m,  int: ℤ,  universe: Type
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  so_lambda: λ2x.t[x],  so_lambda: λ2x y.t[x; y],  so_apply: x[s],  so_apply: x[s1;s2],  subtype_rel: A ⊆r B,  implies: P ⇒ Q,  all: ∀x:A. B[x],  top: Top,  decidable: Dec(P),  or: P ∨ Q,  uimplies: b supposing a,  satisfiable_int_formula: satisfiable_int_formula(fmla),  exists: ∃x:A. B[x],  false: False,  not: ¬A,  prop: ℙ,  le: A ≤ B,  and: P ∧ Q,  nat: ℕ,  uiff: uiff(P;Q),  rev_uimplies: rev_uimplies(P;Q),  ge: i ≥ j ,  guard: {T}
Lemmas referenced :  list_induction,  uall_wf,  le_wf,  absval_wf,  subtract_wf,  list_accum_wf,  list_wf,  list_accum_nil_lemma,  decidable__le,  satisfiable-full-omega-tt,  intformnot_wf,  intformle_wf,  itermVar_wf,  int_formula_prop_not_lemma,  int_formula_prop_le_lemma,  int_term_value_var_lemma,  int_formula_prop_wf,  less_than'_wf,  list_accum_cons_lemma,  nat_wf,  intformand_wf,  itermAdd_wf,  int_formula_prop_and_lemma,  int_term_value_add_lemma,  decidable__equal_int,  intformeq_wf,  itermSubtract_wf,  itermMinus_wf,  int_formula_prop_eq_lemma,  int_term_value_subtract_lemma,  int_term_value_minus_lemma,  add-is-int-iff,  subtract-is-int-iff,  false_wf,  and_wf,  equal_wf,  le_functionality,  le_weakening,  int-triangle-inequality
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  thin,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  hypothesisEquality,  sqequalRule,  lambdaEquality,  intEquality,  because_Cache,  functionEquality,  cumulativity,  addEquality,  applyEquality,  functionExtensionality,  hypothesis,  independent_functionElimination,  dependent_functionElimination,  isect_memberEquality,  voidElimination,  voidEquality,  unionElimination,  natural_numberEquality,  independent_isectElimination,  dependent_pairFormation,  int_eqEquality,  computeAll,  productElimination,  independent_pairEquality,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  lambdaFormation,  rename,  universeEquality,  setElimination,  independent_pairFormation,  pointwiseFunctionality,  promote_hyp,  baseApply,  closedConclusion,  baseClosed,  dependent_set_memberEquality,  setEquality,  hyp_replacement,  Error :applyLambdaEquality
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|))


Date html generated: 2016_10_21-AM-10_01_08
Last ObjectModification: 2016_07_12-AM-05_15_24

Theory : list_1


Home Index