Nuprl Lemma : list_accum-map

∀[L,y,f,g:Top].
  (accumulate (with value x and list item a):
    f[x;a]
   over list:
     map(g;L)
   with starting value:
    y) ~ accumulate (with value x and list item a):
          f[x;g a]
         over list:
           L
         with starting value:
          y))


Proof



Definitions occuring in Statement :  map: map(f;as),  list_accum: list_accum,  uall: ∀[x:A]. B[x],  top: Top,  so_apply: x[s1;s2],  apply: f a,  sqequal: s ~ t
Definitions unfolded in proof :  map: map(f;as),  uall: ∀[x:A]. B[x],  member: t ∈ T,  all: ∀x:A. B[x],  list_ind: list_ind,  nat: ℕ,  implies: P ⇒ Q,  false: False,  ge: i ≥ j ,  guard: {T},  uimplies: b supposing a,  prop: ℙ,  list_accum: list_accum,  so_apply: x[s1;s2],  fun_exp: f^n,  primrec: primrec(n;b;c),  top: Top,  so_lambda: λ2x.t[x],  so_apply: x[s],  decidable: Dec(P),  or: P ∨ Q,  iff: P ⇐⇒ Q,  and: P ∧ Q,  not: ¬A,  rev_implies: P ⇐ Q,  uiff: uiff(P;Q),  subtract: n - m,  subtype_rel: A ⊆r B,  le: A ≤ B,  less_than': less_than'(a;b),  true: True,  nat_plus: ℕ+,  so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]),  so_apply: x[s1;s2;s3;s4],  strict4: strict4(F),  has-value: (a)↓,  squash: ↓T,  cons: [a / b],  so_lambda: λ2x y.t[x; y],  nil: [],  it: ⋅
Lemmas referenced :  nat_properties,  less_than_transitivity1,  less_than_irreflexivity,  ge_wf,  less_than_wf,  base_wf,  strictness-apply,  strictness-callbyvalue,  bottom-sqle,  decidable__le,  subtract_wf,  false_wf,  not-ge-2,  less-iff-le,  condition-implies-le,  minus-one-mul,  zero-add,  minus-one-mul-top,  minus-add,  minus-minus,  add-associates,  add-swap,  add-commutes,  add_functionality_wrt_le,  add-zero,  le-add-cancel,  fun_exp_unroll_1,  lifting-strict-callbyvalue,  has-value_wf_base,  is-exception_wf,  cbv_sqle,  int_subtype_base,  lifting-strict-ispair,  has-value-implies-dec-ispair-2,  top_wf,  lifting-strict-isaxiom,  has-value-implies-dec-isaxiom-2,  cbv_bottom_lemma,  istype-top
Rules used in proof :  sqequalSubstitution,  sqequalRule,  sqequalReflexivity,  sqequalTransitivity,  computationStep,  Error :isect_memberFormation_alt,  introduction,  cut,  thin,  sqequalSqle,  lambdaFormation,  fixpointLeast,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  hypothesisEquality,  hypothesis,  setElimination,  rename,  intWeakElimination,  natural_numberEquality,  independent_isectElimination,  independent_functionElimination,  voidElimination,  lambdaEquality,  dependent_functionElimination,  axiomSqleEquality,  isect_memberEquality,  voidEquality,  unionElimination,  independent_pairFormation,  productElimination,  addEquality,  applyEquality,  intEquality,  minusEquality,  because_Cache,  dependent_set_memberEquality,  baseClosed,  callbyvalueCallbyvalue,  callbyvalueReduce,  baseApply,  closedConclusion,  callbyvalueExceptionCases,  inrFormation,  imageMemberEquality,  imageElimination,  exceptionSqequal,  inlFormation,  sqleReflexivity,  divergentSqle,  axiomSqEquality
Latex:
\mforall{}[L,y,f,g:Top].
    (accumulate  (with  value  x  and  list  item  a):
        f[x;a]
      over  list:
          map(g;L)
      with  starting  value:
        y)  \msim{}  accumulate  (with  value  x  and  list  item  a):
                    f[x;g  a]
                  over  list:
                      L
                  with  starting  value:
                    y))


Date html generated: 2019_06_20-PM-00_39_06
Last ObjectModification: 2018_09_26-PM-02_46_56

Theory : list_0


Home Index