Nuprl Lemma : reduce-as-accum

[T,A:Type]. ∀[f:T ⟶ A ⟶ A].
  ∀[L:T List]. ∀[a:A].
    (reduce(f;a;L) accumulate (with value and list item x): pover list:  Lwith starting value: a) ∈ A) 
  supposing ∀x,y:T. ∀a:A.  ((f (f a)) (f (f a)) ∈ A)


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

\mforall{}[T,A:Type].  \mforall{}[f:T  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    \mforall{}[L:T  List].  \mforall{}[a:A].
        =  accumulate  (with  value  p  and  list  item  x):
              f  x  p
            over  list:
            with  starting  value:
    supposing  \mforall{}x,y:T.  \mforall{}a:A.    ((f  x  (f  y  a))  =  (f  y  (f  x  a)))

Date html generated: 2017_04_17-AM-08_03_06
Last ObjectModification: 2017_02_27-PM-04_33_44

Theory : list_1

Home Index