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

`∀[T:Type]. ∀[as,bs:bag(T)].`
`  uiff(bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs) ∧ (∀z:T. (z ↓∈ as `` (¬z ↓∈ bs)));bag-no-repeats(T;as + bs))`

Proof

Definitions occuring in Statement :  bag-member: `x ↓∈ bs` bag-no-repeats: `bag-no-repeats(T;bs)` bag-append: `as + bs` bag: `bag(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` universe: `Type`
Definitions unfolded in proof :  uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` member: `t ∈ T` bag-no-repeats: `bag-no-repeats(T;bs)` squash: `↓T` prop: `ℙ` uall: `∀[x:A]. B[x]` so_lambda: `λ2x.t[x]` implies: `P `` Q` so_apply: `x[s]` all: `∀x:A. B[x]` not: `¬A` false: `False` cand: `A c∧ B` sq_stable: `SqStable(P)` exists: `∃x:A. B[x]` subtype_rel: `A ⊆r B` bag-append: `as + bs` bag: `bag(T)` quotient: `x,y:A//B[x; y]` iff: `P `⇐⇒` Q` bag-member: `x ↓∈ bs` guard: `{T}` l_disjoint: `l_disjoint(T;l1;l2)`
Lemmas referenced :  bag-no-repeats_wf all_wf bag-member_wf not_wf bag-append_wf bag_wf bag-append-no-repeats1 bag_to_squash_list sq_stable__bag-no-repeats list-subtype-bag no_repeats_functionality_wrt_permutation no_repeats_append_iff equal_wf no_repeats_wf member_wf list_wf append_wf permutation_wf member-permutation
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction cut sqequalRule sqequalHypSubstitution imageElimination hypothesis imageMemberEquality hypothesisEquality thin baseClosed productEquality extract_by_obid isectElimination cumulativity lambdaEquality functionEquality productElimination independent_pairEquality dependent_functionElimination voidElimination because_Cache universeEquality isect_memberEquality equalityTransitivity equalitySymmetry independent_isectElimination independent_functionElimination promote_hyp hyp_replacement applyLambdaEquality rename applyEquality lambdaFormation pertypeElimination dependent_pairFormation

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].
uiff(bag-no-repeats(T;as)
\mwedge{}  bag-no-repeats(T;bs)
\mwedge{}  (\mforall{}z:T.  (z  \mdownarrow{}\mmember{}  as  {}\mRightarrow{}  (\mneg{}z  \mdownarrow{}\mmember{}  bs)));bag-no-repeats(T;as  +  bs))

Date html generated: 2017_10_01-AM-08_59_13
Last ObjectModification: 2017_07_26-PM-04_41_13

Theory : bags

Home Index