### Nuprl Lemma : bag-product-single

`∀[bs:Top List]. ∀[a:Top].  ({a} × bs ~ bag-map(λx.<a, x>;bs))`

Proof

Definitions occuring in Statement :  bag-product: `bs × cs` bag-map: `bag-map(f;bs)` single-bag: `{x}` list: `T List` uall: `∀[x:A]. B[x]` top: `Top` lambda: `λx.A[x]` pair: `<a, b>` sqequal: `s ~ t`
Definitions unfolded in proof :  bag-map: `bag-map(f;bs)` single-bag: `{x}` bag-product: `bs × cs` all: `∀x:A. B[x]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` member: `t ∈ T` top: `Top` so_apply: `x[s1;s2;s3]` empty-bag: `{}` bag-append: `as + bs` uall: `∀[x:A]. B[x]`
Lemmas referenced :  list_ind_cons_lemma list_ind_nil_lemma append_back_nil top_wf map_wf list_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis isect_memberFormation introduction isectElimination productEquality lambdaEquality independent_pairEquality hypothesisEquality sqequalAxiom because_Cache

Latex:
\mforall{}[bs:Top  List].  \mforall{}[a:Top].    (\{a\}  \mtimes{}  bs  \msim{}  bag-map(\mlambda{}x.<a,  x>bs))

Date html generated: 2016_05_15-PM-02_22_52
Last ObjectModification: 2015_12_27-AM-09_54_34

Theory : bags

Home Index