### Nuprl Lemma : bag-combine-size

`∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[ba:bag(A)].  (#(⋃a∈ba.f[a]) = bag-sum(ba;a.#(f[a])) ∈ ℕ)`

Proof

Definitions occuring in Statement :  bag-sum: `bag-sum(ba;x.f[x])` bag-combine: `⋃x∈bs.f[x]` bag-size: `#(bs)` bag: `bag(T)` nat: `ℕ` uall: `∀[x:A]. B[x]` so_apply: `x[s]` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` bag: `bag(T)` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` all: `∀x:A. B[x]` implies: `P `` Q` uimplies: `b supposing a` nat: `ℕ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` sq_type: `SQType(T)` guard: `{T}` prop: `ℙ` bag-combine: `⋃x∈bs.f[x]` bag-size: `#(bs)` bag-sum: `bag-sum(ba;x.f[x])` bag-map: `bag-map(f;bs)` bag-union: `bag-union(bbs)` concat: `concat(ll)` false: `False` ge: `i ≥ j ` not: `¬A` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` top: `Top` or: `P ∨ Q` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` decidable: `Dec(P)` le: `A ≤ B` less_than': `less_than'(a;b)` cons: `[a / b]` colength: `colength(L)` nil: `[]` it: `⋅` less_than: `a < b` squash: `↓T` subtype_rel: `A ⊆r B` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  nat_wf subtype_base_sq set_subtype_base le_wf istype-int int_subtype_base permutation_wf list_wf bag_wf istype-universe nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma istype-void int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf ge_wf istype-less_than list-cases list_accum_nil_lemma map_nil_lemma reduce_nil_lemma length_of_nil_lemma decidable__equal_int intformnot_wf intformeq_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma istype-false istype-le product_subtype_list colength-cons-not-zero istype-nat colength_wf_list subtract-1-ge-0 spread_cons_lemma subtract_wf itermSubtract_wf itermAdd_wf int_term_value_subtract_lemma int_term_value_add_lemma decidable__le list_accum_cons_lemma map_cons_lemma reduce_cons_lemma length-append bag-size_wf zero-le-nat list_accum_wf add_nat_wf add-swap add-commutes equal_wf iff_weakening_equal trivial-equal quotient-member-eq permutation-equiv bag-combine_wf list-subtype-bag equal-wf-base
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality extract_by_obid hypothesis sqequalRule pertypeElimination productElimination thin equalityTransitivity equalitySymmetry inhabitedIsType lambdaFormation_alt rename instantiate isectElimination cumulativity independent_isectElimination intEquality lambdaEquality_alt closedConclusion natural_numberEquality hypothesisEquality dependent_functionElimination independent_functionElimination universeIsType equalityIsType1 productIsType equalityIsType4 because_Cache isect_memberEquality_alt axiomEquality isectIsTypeImplies functionIsType universeEquality setElimination intWeakElimination approximateComputation dependent_pairFormation_alt int_eqEquality voidElimination independent_pairFormation functionIsTypeImplies unionElimination dependent_set_memberEquality_alt promote_hyp hypothesis_subsumption applyLambdaEquality imageElimination baseApply baseClosed applyEquality addEquality imageMemberEquality hyp_replacement

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[ba:bag(A)].    (\#(\mcup{}a\mmember{}ba.f[a])  =  bag-sum(ba;a.\#(f[a])))

Date html generated: 2019_10_15-AM-11_00_28
Last ObjectModification: 2018_10_18-PM-11_34_06

Theory : bags

Home Index