Nuprl Lemma : accum_list_cons_lemma

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


Proof



Definitions occuring in Statement :  accum_list: accum_list(a,x.f[a; x];x.base[x];L),  list_accum: list_accum,  cons: [a / b],  top: Top,  so_apply: x[s1;s2],  so_apply: x[s],  all: ∀x:A. B[x],  sqequal: s ~ t
Definitions unfolded in proof :  all: ∀x:A. B[x],  member: t ∈ T,  accum_list: accum_list(a,x.f[a; x];x.base[x];L),  top: Top
Lemmas referenced :  top_wf,  reduce_hd_cons_lemma,  reduce_tl_cons_lemma
Rules used in proof :  sqequalSubstitution,  sqequalTransitivity,  computationStep,  sqequalReflexivity,  lambdaFormation,  cut,  hypothesis,  lemma_by_obid,  sqequalRule,  sqequalHypSubstitution,  dependent_functionElimination,  thin,  isect_memberEquality,  voidElimination,  voidEquality
Latex:
\mforall{}L,u,base,f:Top.
    (accum\_list(a,x.f[a;x];  y.base[y];  [u  /  L])  \msim{}  accumulate  (with  value  a  and  list  item  y):
                                                                                                  f[a;y]
                                                                                                over  list:
                                                                                                    L
                                                                                                with  starting  value:
                                                                                                  base[u]))


Date html generated: 2016_05_14-AM-07_40_00
Last ObjectModification: 2015_12_26-PM-02_13_45

Theory : list_1


Home Index