### Nuprl Lemma : bag-accum-single

`∀[init,f,x:Top].  (bag-accum(v,x.f[v;x];init;{x}) ~ f[init;x])`

Proof

Definitions occuring in Statement :  bag-accum: `bag-accum(v,x.f[v; x];init;bs)` single-bag: `{x}` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s1;s2]` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` single-bag: `{x}` bag-accum: `bag-accum(v,x.f[v; x];init;bs)` all: `∀x:A. B[x]` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  list_accum_cons_lemma list_accum_nil_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis sqequalAxiom isectElimination hypothesisEquality because_Cache

Latex:
\mforall{}[init,f,x:Top].    (bag-accum(v,x.f[v;x];init;\{x\})  \msim{}  f[init;x])

Date html generated: 2016_05_15-PM-02_30_07
Last ObjectModification: 2015_12_27-AM-09_49_04

Theory : bags

Home Index