Nuprl Lemma : list_accum-remove-repeats

∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
  (∀[as: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:
         remove-repeats(eq;as)
       with starting value:
        n)
     ∈ A)) supposing 
     ((∀x:A. (f[x;x] = x ∈ A)) and 
     Assoc(A;λx,y. f[x;y]) and 
     Comm(A;λx,y. f[x;y]))


Proof



Definitions occuring in Statement :  remove-repeats: remove-repeats(eq;L),  list_accum: list_accum,  list: T List,  deq: EqDecider(T),  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],  all: ∀x:A. B[x],  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],  so_lambda: λ2x y.t[x; y],  so_apply: x[s1;s2],  so_apply: x[s],  implies: P ⇒ Q,  list_accum: list_accum,  nil: [],  it: ⋅,  remove-repeats: remove-repeats(eq;L),  list_ind: list_ind,  all: ∀x:A. B[x],  prop: ℙ,  top: Top,  squash: ↓T,  deq: EqDecider(T),  true: True,  subtype_rel: A ⊆r B,  guard: {T},  iff: P ⇐⇒ Q,  and: P ∧ Q,  rev_implies: P ⇐ Q,  bool: 𝔹,  unit: Unit,  btrue: tt,  uiff: uiff(P;Q),  eqof: eqof(d),  bnot: ¬bb,  ifthenelse: if b then t else f fi ,  bfalse: ff,  exists: ∃x:A. B[x],  or: P ∨ Q,  sq_type: SQType(T),  assert: ↑b,  false: False,  not: ¬A,  assoc: Assoc(T;op),  infix_ap: x f y,  comm: Comm(T;op)
Lemmas referenced :  list_induction,  uall_wf,  equal_wf,  list_accum_wf,  remove-repeats_wf,  list_wf,  nil_wf,  all_wf,  assoc_wf,  comm_wf,  deq_wf,  list_accum_cons_lemma,  remove_repeats_cons_lemma,  squash_wf,  true_wf,  filter_wf5,  l_member_wf,  bnot_wf,  iff_weakening_equal,  list_accum_nil_lemma,  filter_nil_lemma,  filter_cons_lemma,  bool_wf,  eqtt_to_assert,  safe-assert-deq,  eqff_to_assert,  bool_cases_sqequal,  subtype_base_sq,  bool_subtype_base,  assert-bnot,  deq_property,  and_wf
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  isect_memberFormation,  introduction,  cut,  thin,  extract_by_obid,  sqequalHypSubstitution,  isectElimination,  hypothesisEquality,  sqequalRule,  lambdaEquality,  cumulativity,  applyEquality,  functionExtensionality,  hypothesis,  independent_functionElimination,  because_Cache,  lambdaFormation,  rename,  dependent_functionElimination,  isect_memberEquality,  axiomEquality,  equalityTransitivity,  equalitySymmetry,  functionEquality,  universeEquality,  voidElimination,  voidEquality,  imageElimination,  setElimination,  setEquality,  natural_numberEquality,  imageMemberEquality,  baseClosed,  independent_isectElimination,  productElimination,  unionElimination,  equalityElimination,  dependent_pairFormation,  promote_hyp,  instantiate,  hyp_replacement,  dependent_set_memberEquality,  independent_pairFormation,  applyLambdaEquality
Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[A:Type].  \mforall{}[g:T  {}\mrightarrow{}  A].  \mforall{}[f:A  {}\mrightarrow{}  A  {}\mrightarrow{}  A].
    (\mforall{}[as: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:
                  remove-repeats(eq;as)
              with  starting  value:
                n)))  supposing 
          ((\mforall{}x:A.  (f[x;x]  =  x))  and 
          Assoc(A;\mlambda{}x,y.  f[x;y])  and 
          Comm(A;\mlambda{}x,y.  f[x;y]))


Date html generated: 2017_04_17-AM-09_11_48
Last ObjectModification: 2017_02_27-PM-05_19_17

Theory : decidable!equality


Home Index