Nuprl Lemma : bag-sum_wf

`∀[A:Type]. ∀[f:A ⟶ ℤ]. ∀[ba:bag(A)].  (bag-sum(ba;x.f[x]) ∈ ℤ)`

Proof

Definitions occuring in Statement :  bag-sum: `bag-sum(ba;x.f[x])` bag: `bag(T)` uall: `∀[x:A]. B[x]` so_apply: `x[s]` member: `t ∈ T` function: `x:A ⟶ B[x]` int: `ℤ` universe: `Type`
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` bag-sum: `bag-sum(ba;x.f[x])` so_lambda: `λ2x.t[x]` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s]` so_apply: `x[s1;s2]` prop: `ℙ` squash: `↓T` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` decidable: `Dec(P)` or: `P ∨ Q` uimplies: `b supposing a` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` append: `as @ bs` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` subtype_rel: `A ⊆r B` guard: `{T}`
Lemmas referenced :  list_wf permutation-invariant equal_wf list_accum_wf squash_wf true_wf cons_wf decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf intformimplies_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formual_prop_imp_lemma int_formula_prop_wf permutation_wf equal-wf-base bag_wf list_induction all_wf append_wf nil_wf list_ind_nil_lemma list_accum_cons_lemma list_accum_nil_lemma list_ind_cons_lemma iff_weakening_equal itermAdd_wf int_term_value_add_lemma itermConstant_wf int_term_value_constant_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution pointwiseFunctionalityForEquality intEquality sqequalRule pertypeElimination productElimination thin equalityTransitivity hypothesis equalitySymmetry extract_by_obid isectElimination cumulativity hypothesisEquality lambdaFormation because_Cache rename lambdaEquality natural_numberEquality addEquality applyEquality functionExtensionality independent_functionElimination addLevel hyp_replacement imageElimination equalityUniverse levelHypothesis imageMemberEquality baseClosed dependent_functionElimination unionElimination independent_isectElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll productEquality axiomEquality functionEquality universeEquality

Latex:
\mforall{}[A:Type].  \mforall{}[f:A  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[ba:bag(A)].    (bag-sum(ba;x.f[x])  \mmember{}  \mBbbZ{})

Date html generated: 2017_10_01-AM-08_47_52
Last ObjectModification: 2017_07_26-PM-04_32_12

Theory : bags

Home Index