### Nuprl Lemma : bag-combine-assoc

[f,g:Top]. ∀[bs:bag(Top)].  (⋃y∈⋃x∈bs.f[x].g[y] ~ ⋃x∈bs.⋃y∈f[x].g[y])

Proof

Definitions occuring in Statement :  bag-combine: x∈bs.f[x] bag: bag(T) uall: [x:A]. B[x] top: Top so_apply: x[s] sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag-combine: x∈bs.f[x] bag-map: bag-map(f;bs) bag-union: bag-union(bbs) top: Top subtype_rel: A ⊆B all: x:A. B[x]
Lemmas referenced :  concat-map-assoc bag-subtype-list bag_wf top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin isect_memberEquality voidElimination voidEquality hypothesisEquality applyEquality dependent_functionElimination because_Cache hypothesis sqequalAxiom

Latex:
\mforall{}[f,g:Top].  \mforall{}[bs:bag(Top)].    (\mcup{}y\mmember{}\mcup{}x\mmember{}bs.f[x].g[y]  \msim{}  \mcup{}x\mmember{}bs.\mcup{}y\mmember{}f[x].g[y])

Date html generated: 2016_05_15-PM-02_28_09
Last ObjectModification: 2015_12_27-AM-09_50_58

Theory : bags

Home Index