### Nuprl Lemma : bag-product-no-repeats

`∀[A,B:Type]. ∀[as:bag(A)]. ∀[bs:bag(B)].`
`  bag-no-repeats(A × B;as × bs) supposing bag-no-repeats(A;as) ∧ bag-no-repeats(B;bs)`

Proof

Definitions occuring in Statement :  bag-no-repeats: `bag-no-repeats(T;bs)` bag-product: `bs × cs` bag: `bag(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` and: `P ∧ Q` product: `x:A × B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` bag-no-repeats: `bag-no-repeats(T;bs)` squash: `↓T` prop: `ℙ` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_stable: `SqStable(P)` exists: `∃x:A. B[x]` empty-bag: `{}` top: `Top` cons-bag: `x.b` uiff: `uiff(P;Q)` cand: `A c∧ B` not: `¬A` false: `False` inject: `Inj(A;B;f)` pi2: `snd(t)` guard: `{T}`
Lemmas referenced :  bag-no-repeats_wf bag_wf bag-product_wf squash_wf nil_wf list-subtype-bag cons_wf all_wf bag_to_squash_list sq_stable__all sq_stable__bag-no-repeats list_induction list_wf bag-product-empty empty-bag-no-repeats cons-bag-as-append bag-product-append single-bag_wf bag-subtype-list subtype_rel_list top_wf bag-append-no-repeats bag-member_wf bag-product-single bag-map-no-repeats and_wf equal_wf pi2_wf bag-member-product pi1_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution productElimination thin dependent_functionElimination hypothesisEquality hypothesis independent_functionElimination sqequalRule imageElimination imageMemberEquality baseClosed productEquality extract_by_obid isectElimination cumulativity isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality lambdaEquality functionEquality lambdaFormation voidEquality applyEquality independent_isectElimination voidElimination promote_hyp hyp_replacement Error :applyLambdaEquality,  rename independent_pairFormation independent_pairEquality dependent_set_memberEquality setElimination setEquality

Latex:
\mforall{}[A,B:Type].  \mforall{}[as:bag(A)].  \mforall{}[bs:bag(B)].
bag-no-repeats(A  \mtimes{}  B;as  \mtimes{}  bs)  supposing  bag-no-repeats(A;as)  \mwedge{}  bag-no-repeats(B;bs)

Date html generated: 2016_10_25-AM-10_32_40
Last ObjectModification: 2016_07_12-AM-06_48_44

Theory : bags

Home Index