Nuprl Lemma : list_accum_functionality

∀[T,A:Type]. ∀[f,g:T ⟶ A ⟶ T]. ∀[L:A List]. ∀[y,z:T].
  (accumulate (with value x and list item a):
    f[x;a]
   over list:
     L
   with starting value:
    y)
     = accumulate (with value x and list item a):
        g[x;a]
       over list:
         L
       with starting value:
        z)
     ∈ T) supposing 
     ((y = z ∈ T) and 
     (∀L':A List. ∀a:A.
        (L' @ [a] ≤ L
        ⇒ (f[accumulate (with value x and list item a):
               f[x;a]
              over list:
                L'
              with starting value:
               y);a]
           = g[accumulate (with value x and list item a):
                f[x;a]
               over list:
                 L'
               with starting value:
                y);a]
           ∈ T))))


Proof



Definitions occuring in Statement :  iseg: l1 ≤ l2,  append: as @ bs,  list_accum: list_accum,  cons: [a / b],  nil: [],  list: T List,  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2],  all: ∀x:A. B[x],  implies: P ⇒ Q,  function: x:A ⟶ B[x],  universe: Type,  equal: s = t ∈ T
Definitions unfolded in proof :  uall: ∀[x:A]. B[x],  member: t ∈ T,  uimplies: b supposing a,  so_lambda: λ2x.t[x],  implies: P ⇒ Q,  prop: ℙ,  so_apply: x[s],  so_apply: x[s1;s2],  all: ∀x:A. B[x],  so_lambda: λ2x y.t[x; y],  guard: {T},  top: Top,  subtype_rel: A ⊆r B,  squash: ↓T,  true: True,  iff: P ⇐⇒ Q,  and: P ∧ Q,  rev_implies: P ⇐ Q
Lemmas referenced :  last_induction,  all_wf,  equal_wf,  list_accum_wf,  list_wf,  iseg_wf,  append_wf,  cons_wf,  nil_wf,  list_accum_nil_lemma,  subtype_rel_list,  top_wf,  list_accum_cons_lemma,  list_accum_append,  squash_wf,  true_wf,  iseg_weakening,  iff_weakening_equal,  iseg_append
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  thin,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  hypothesisEquality,  sqequalRule,  lambdaEquality,  cumulativity,  because_Cache,  functionEquality,  hypothesis,  applyEquality,  functionExtensionality,  independent_functionElimination,  dependent_functionElimination,  isect_memberEquality,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  voidElimination,  voidEquality,  lambdaFormation,  independent_isectElimination,  imageElimination,  natural_numberEquality,  imageMemberEquality,  baseClosed,  universeEquality,  productElimination,  hyp_replacement,  applyLambdaEquality
Latex:
\mforall{}[T,A:Type].  \mforall{}[f,g:T  {}\mrightarrow{}  A  {}\mrightarrow{}  T].  \mforall{}[L:A  List].  \mforall{}[y,z:T].
    (accumulate  (with  value  x  and  list  item  a):
        f[x;a]
      over  list:
          L
      with  starting  value:
        y)
          =  accumulate  (with  value  x  and  list  item  a):
                g[x;a]
              over  list:
                  L
              with  starting  value:
                z))  supposing 
          ((y  =  z)  and 
          (\mforall{}L':A  List.  \mforall{}a:A.
                (L'  @  [a]  \mleq{}  L
                {}\mRightarrow{}  (f[accumulate  (with  value  x  and  list  item  a):
                              f[x;a]
                            over  list:
                                L'
                            with  starting  value:
                              y);a]
                      =  g[accumulate  (with  value  x  and  list  item  a):
                                f[x;a]
                              over  list:
                                  L'
                              with  starting  value:
                                y);a]))))


Date html generated: 2017_04_17-AM-07_37_35
Last ObjectModification: 2017_02_27-PM-04_11_59

Theory : list_1


Home Index