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

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

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs:bag(T)].
bag-no-repeats(T;as  +  bs)
supposing  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)))

Date html generated: 2017_10_01-AM-08_59_04
Last ObjectModification: 2017_07_26-PM-04_41_08

Theory : bags

Home Index