### Nuprl Lemma : bag-member-splits

`∀[T:Type]. ∀[as,bs,cs:bag(T)].  uiff(<as, bs> ↓∈ bag-splits(cs);(as + bs) = cs ∈ bag(T))`

Proof

Definitions occuring in Statement :  bag-splits: `bag-splits(b)` bag-member: `x ↓∈ bs` bag-append: `as + bs` bag: `bag(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` pair: `<a, b>` product: `x:A × B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` all: `∀x:A. B[x]` prop: `ℙ` bag-member: `x ↓∈ bs` squash: `↓T` subtype_rel: `A ⊆r B` true: `True` quotient: `x,y:A//B[x; y]` bag: `bag(T)` istype: `istype(T)` implies: `P `` Q` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` iff: `P `⇐⇒` Q` guard: `{T}` cand: `A c∧ B` exists: `∃x:A. B[x]` decidable: `Dec(P)` less_than: `a < b` sq_type: `SQType(T)` so_apply: `x[s]` so_lambda: `λ2x.t[x]` it: `⋅` nil: `[]` colength: `colength(L)` less_than': `less_than'(a;b)` le: `A ≤ B` cons: `[a / b]` so_apply: `x[s1;s2;s3]` so_lambda: so_lambda3 bag-splits: `bag-splits(b)` or: `P ∨ Q` top: `Top` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` ge: `i ≥ j ` false: `False` nat: `ℕ` pi2: `snd(t)` pi1: `fst(t)` single-bag: `{x}` empty-bag: `{}` append: `as @ bs` bag-append: `as + bs` bag-map: `bag-map(f;bs)` rev_implies: `P `` Q` remove-nth: `remove-nth(n;L)` lelt: `i ≤ j < k` int_seg: `{i..j-}` int_iseg: `{i...j}` subtract: `n - m` tl: `tl(l)` lt_int: `i <z j` le_int: `i ≤z j` nth_tl: `nth_tl(n;as)` assert: `↑b` bnot: `¬bb` bfalse: `ff` ifthenelse: `if b then t else f fi ` btrue: `tt` unit: `Unit` bool: `𝔹` respects-equality: `respects-equality(S;T)` select: `L[n]` add-nth: `add-nth(n;x;L)`
Lemmas referenced :  bag-member_wf bag_wf bag-splits_wf bag-append_wf istype-universe subtype_rel_self true_wf squash_wf equal_wf permutation_weakening permutation_wf list_wf list-subtype-bag permutation-equiv quotient-member-eq l_member_wf member-permutation bag-splits_wf_list istype-nat cons_wf list_ind_cons_lemma le_wf decidable__le int_term_value_add_lemma int_term_value_subtract_lemma int_formula_prop_not_lemma itermAdd_wf itermSubtract_wf intformnot_wf subtract_wf decidable__equal_int spread_cons_lemma int_subtype_base set_subtype_base int_formula_prop_eq_lemma intformeq_wf subtype_base_sq subtract-1-ge-0 istype-le istype-false colength_wf_list colength-cons-not-zero product_subtype_list nil_wf list_ind_nil_lemma list-cases istype-less_than ge_wf int_formula_prop_wf int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma istype-void int_formula_prop_and_lemma istype-int intformless_wf itermVar_wf itermConstant_wf intformle_wf intformand_wf full-omega-unsat nat_properties empty-bag_wf member_singleton equal-empty-bag empty_bag_append_lemma bag-append-assoc-comm bag-append-assoc single-bag_wf map_wf member_append member_map bag_to_squash_list append_wf equal-wf-base permutation_inversion list_induction append_is_nil permutation-nil-iff iff_weakening_equal trivial-equal permutation-cons pi1_wf pi2_wf false_wf add-is-int-iff add_nat_wf decidable__lt non_neg_length length-append remove-nth_wf length_wf_nat length_of_cons_lemma top_wf subtype_rel_list length_append length_wf firstn-append nth_tl-append bfalse_wf btrue_wf le_weakening2 length_firstn length_firstn_eq nth_tl_wf firstn_wf ifthenelse_wf general-append-cancellation firstn_all le_int_wf less_than_wf assert_wf bool_wf iff_weakening_uiff assert-bnot bool_subtype_base bool_cases_sqequal eqff_to_assert assert_of_le_int assert_of_lt_int eqtt_to_assert lt_int_wf respects-equality-product respects-equality-list-bag respects-equality-trivial istype-base bnot_wf not_wf istype-assert bool_cases iff_transitivity assert_of_bnot append_assoc_sq nil-append nth_tl_is_nil minus-one-mul add-mul-special zero-mul bag-append-comm select_wf select-append add-remove-nth firstn_append firstn_firstn add-zero add-commutes add-associates add-swap nth_tl_nth_tl subtype-respects-equality general_arith_equation1 first0 append-nil zero-add minus-minus minus-add
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut independent_pairFormation hypothesis universeIsType extract_by_obid sqequalHypSubstitution isectElimination thin productEquality hypothesisEquality independent_pairEquality dependent_functionElimination sqequalRule imageElimination imageMemberEquality baseClosed equalityIstype inhabitedIsType productElimination isect_memberEquality_alt axiomEquality isectIsTypeImplies instantiate universeEquality natural_numberEquality equalityTransitivity lambdaEquality_alt applyEquality equalitySymmetry sqequalBase productIsType pertypeElimination pointwiseFunctionality independent_isectElimination because_Cache lambdaFormation_alt promote_hyp applyLambdaEquality hyp_replacement independent_functionElimination intEquality closedConclusion baseApply dependent_set_memberEquality_alt hypothesis_subsumption unionElimination functionIsTypeImplies voidElimination int_eqEquality dependent_pairFormation_alt approximateComputation intWeakElimination rename setElimination functionEquality Error :memTop,  functionIsType voidEquality inlFormation_alt inrFormation_alt addEquality cumulativity equalityElimination multiplyEquality minusEquality

Latex:
\mforall{}[T:Type].  \mforall{}[as,bs,cs:bag(T)].    uiff(<as,  bs>  \mdownarrow{}\mmember{}  bag-splits(cs);(as  +  bs)  =  cs)

Date html generated: 2020_05_20-AM-08_02_34
Last ObjectModification: 2019_12_31-PM-10_16_27

Theory : bags

Home Index