Nuprl Lemma : list_accum_is_reduce

[A:Type]. ∀[f:A ⟶ A ⟶ A].
  (∀[as:A List]. ∀[n:A].
     (accumulate (with value and list item b):
      over list:
      with starting value:
     ∈ A)) supposing 
     (Assoc(A;λx,y. f[x;y]) and 
     Comm(A;λx,y. f[x;y]))


Definitions occuring in Statement :  reduce: reduce(f;k;as) list_accum: list_accum list: List comm: Comm(T;op) assoc: Assoc(T;op) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a prop: so_apply: x[s1;s2] all: x:A. B[x] true: True squash: T so_lambda: λ2y.t[x; y] subtype_rel: A ⊆B guard: {T} iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q implies:  Q assoc: Assoc(T;op) infix_ap: y comm: Comm(T;op)
Lemmas referenced :  list_wf assoc_wf comm_wf reduce_wf equal_wf squash_wf true_wf list_accum_as_reduce iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis hypothesisEquality sqequalRule sqequalHypSubstitution isect_memberEquality isectElimination thin axiomEquality because_Cache extract_by_obid cumulativity lambdaEquality applyEquality functionExtensionality equalityTransitivity equalitySymmetry functionEquality universeEquality lambdaFormation natural_numberEquality imageElimination independent_isectElimination imageMemberEquality baseClosed productElimination independent_functionElimination

\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[as:A  List].  \mforall{}[n:A].
          (accumulate  (with  value  a  and  list  item  b):
            over  list:
            with  starting  value:
          =  reduce(f;n;as)))  supposing 
          (Assoc(A;\mlambda{}x,y.  f[x;y])  and 
          Comm(A;\mlambda{}x,y.  f[x;y]))

Date html generated: 2017_04_17-AM-07_38_25
Last ObjectModification: 2017_02_27-PM-04_11_28

Theory : list_1

Home Index