### Nuprl Lemma : bag-summation-map

`∀[add,zero:Top]. ∀[b:Top List]. ∀[f,g:Top].  (Σ(x∈bag-map(g;b)). f[x] ~ Σ(x∈b). f[g x])`

Proof

Definitions occuring in Statement :  bag-summation: `Σ(x∈b). f[x]` bag-map: `bag-map(f;bs)` list: `T List` uall: `∀[x:A]. B[x]` top: `Top` so_apply: `x[s]` apply: `f a` sqequal: `s ~ t`
Definitions unfolded in proof :  bag-summation: `Σ(x∈b). f[x]` uall: `∀[x:A]. B[x]` member: `t ∈ T` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]`
Lemmas referenced :  bag-accum-map top_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity sqequalRule cut lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesisEquality hypothesis because_Cache isect_memberFormation introduction sqequalAxiom

Latex:
\mforall{}[add,zero:Top].  \mforall{}[b:Top  List].  \mforall{}[f,g:Top].    (\mSigma{}(x\mmember{}bag-map(g;b)).  f[x]  \msim{}  \mSigma{}(x\mmember{}b).  f[g  x])

Date html generated: 2016_05_15-PM-02_32_24
Last ObjectModification: 2015_12_27-AM-09_47_39

Theory : bags

Home Index