Nuprl Lemma : list_accum_set-equal

∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
  (∀[as,bs:T List].
     (∀[n:A]
        (accumulate (with value a and list item z):
          f[a;g[z]]
         over list:
           as
         with starting value:
          n)
        = accumulate (with value a and list item z):
           f[a;g[z]]
          over list:
            bs
          with starting value:
           n)
        ∈ A)) supposing 
        (no_repeats(T;bs) and 
        no_repeats(T;as) and 
        set-equal(T;as;bs))) supposing 
     (Assoc(A;λx,y. f[x;y]) and 
     Comm(A;λx,y. f[x;y]))


Proof



Definitions occuring in Statement :  set-equal: set-equal(T;x;y),  no_repeats: no_repeats(T;l),  list_accum: list_accum,  list: T List,  comm: Comm(T;op),  assoc: Assoc(T;op),  uimplies: b supposing a,  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2],  so_apply: x[s],  lambda: λx.A[x],  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],  prop: ℙ,  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  so_apply: x[s],  implies: P ⇒ Q,  all: ∀x:A. B[x],  top: Top,  or: P ∨ Q,  cons: [a / b],  set-equal: set-equal(T;x;y),  iff: P ⇐⇒ Q,  and: P ∧ Q,  rev_implies: P ⇐ Q,  false: False,  exists: ∃x:A. B[x],  squash: ↓T,  true: True,  subtype_rel: A ⊆r B,  guard: {T},  append: as @ bs,  so_lambda: so_lambda(x,y,z.t[x; y; z]),  so_apply: x[s1;s2;s3],  equiv_rel: EquivRel(T;x,y.E[x; y]),  trans: Trans(T;x,y.E[x; y]),  uiff: uiff(P;Q),  rev_uimplies: rev_uimplies(P;Q),  cand: A c∧ B,  l_disjoint: l_disjoint(T;l1;l2),  not: ¬A
Lemmas referenced :  list_induction,  uall_wf,  list_wf,  isect_wf,  set-equal_wf,  no_repeats_wf,  equal_wf,  list_accum_wf,  list_accum_nil_lemma,  nil_wf,  list_accum_cons_lemma,  cons_wf,  assoc_wf,  comm_wf,  list-cases,  product_subtype_list,  nil_member,  false_wf,  l_member_wf,  cons_member,  set-equal-cons,  length_wf_nat,  nat_wf,  list_accum_permute,  squash_wf,  true_wf,  iff_weakening_equal,  list_ind_cons_lemma,  append_wf,  set-equal-equiv,  set-equal-permute,  no_repeats_cons,  no_repeats_append_iff
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  thin,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  hypothesisEquality,  sqequalRule,  lambdaEquality,  cumulativity,  hypothesis,  because_Cache,  applyEquality,  functionExtensionality,  independent_functionElimination,  dependent_functionElimination,  isect_memberEquality,  voidElimination,  voidEquality,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  lambdaFormation,  rename,  functionEquality,  universeEquality,  unionElimination,  promote_hyp,  hypothesis_subsumption,  productElimination,  independent_pairFormation,  inlFormation,  independent_isectElimination,  dependent_set_memberEquality,  comment,  hyp_replacement,  applyLambdaEquality,  setElimination,  imageElimination,  natural_numberEquality,  imageMemberEquality,  baseClosed,  inrFormation,  productEquality
Latex:
\mforall{}[T,A:Type].  \mforall{}[g:T  {}\mrightarrow{}  A].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[as,bs:T  List].
          (\mforall{}[n:A]
                (accumulate  (with  value  a  and  list  item  z):
                    f[a;g[z]]
                  over  list:
                      as
                  with  starting  value:
                    n)
                =  accumulate  (with  value  a  and  list  item  z):
                      f[a;g[z]]
                    over  list:
                        bs
                    with  starting  value:
                      n)))  supposing 
                (no\_repeats(T;bs)  and 
                no\_repeats(T;as)  and 
                set-equal(T;as;bs)))  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_16
Last ObjectModification: 2017_02_27-PM-04_11_53

Theory : list_1


Home Index