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

`∀[T:Type]. ∀[as,bs:bag(T)].`
`  uiff(bag-no-repeats(T;as + bs);bag-no-repeats(T;as) ∧ bag-no-repeats(T;bs) ∧ (∀x:T. (x ↓∈ as `` (¬x ↓∈ 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]` rev_implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` implies: `P `` Q` all: `∀x:A. B[x]` iff: `P `⇐⇒` Q` not: `¬A` false: `False`
Lemmas referenced :  bag_wf uiff_wf bag-append-no-repeats bag-member_wf not_wf rev_implies_wf all_wf and_wf iff_weakening_uiff bag-append_wf bag-no-repeats_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity independent_pairFormation isect_memberFormation introduction hypothesis sqequalRule sqequalHypSubstitution imageElimination imageMemberEquality hypothesisEquality thin baseClosed lemma_by_obid isectElimination because_Cache addLevel productElimination independent_isectElimination lambdaEquality independent_functionElimination independent_pairEquality dependent_functionElimination voidElimination cumulativity functionEquality universeEquality isect_memberEquality equalityTransitivity equalitySymmetry

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

Date html generated: 2016_05_15-PM-02_56_04
Last ObjectModification: 2016_01_16-AM-08_39_39

Theory : bags

Home Index