Nuprl Lemma : bag-summation-partition

[A:Type]
  ∀[R,T:Type]. ∀[add:R ⟶ R ⟶ R]. ∀[zero:R]. ∀[b:bag(T)]. ∀[case:T ⟶ A ⟶ 𝔹]. ∀[f:T ⟶ R]. ∀[c:bag(A)].
    Σ(x∈b). f[x] = Σ(z∈c). Σ(x∈[x∈b|case[x;z]]). f[x] ∈ 
    supposing (IsMonoid(R;add;zero) ∧ Comm(R;add))
    ∧ (∀x:{x:T| x ↓∈ b} (∃z:{A| (z ↓∈ c ∧ (↑case[x;z]))}))
    ∧ bag-no-repeats(A;c)
    ∧ (∀z1,z2:A. ∀x:T.  ((↑case[x;z1])  (↑case[x;z2])  (z1 z2 ∈ A))) 
  supposing ∀x,y:A.  Dec(x y ∈ A)


Proof




Definitions occuring in Statement :  bag-member: x ↓∈ bs bag-no-repeats: bag-no-repeats(T;bs) bag-summation: Σ(x∈b). f[x] bag-filter: [x∈b|p[x]] bag: bag(T) comm: Comm(T;op) assert: b bool: 𝔹 decidable: Dec(P) uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s1;s2] so_apply: x[s] all: x:A. B[x] sq_exists: x:{A| B[x]} implies:  Q and: P ∧ Q set: {x:A| B[x]}  function: x:A ⟶ B[x] universe: Type equal: t ∈ T monoid_p: IsMonoid(T;op;id)
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a and: P ∧ Q squash: T exists: x:A. B[x] prop: so_lambda: λ2x.t[x] so_apply: x[s1;s2] so_apply: x[s] implies:  Q subtype_rel: A ⊆B all: x:A. B[x] sq_exists: x:{A| B[x]} cand: c∧ B monoid_p: IsMonoid(T;op;id) bag-filter: [x∈b|p[x]] top: Top empty-bag: {} true: True guard: {T} iff: ⇐⇒ Q rev_implies:  Q cons-bag: x.b uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) sq_or: a ↓∨ b or: P ∨ Q single-bag: {x} bag-append: as bs append: as bs so_lambda: so_lambda(x,y,z.t[x; y; z]) so_apply: x[s1;s2;s3] infix_ap: y bag-member: x ↓∈ bs sq_type: SQType(T) assert: b ifthenelse: if then else fi  btrue: tt
Lemmas referenced :  bag_to_squash_list all_wf bag-member_wf sq_exists_wf assert_wf list_induction list-subtype-bag equal_wf bag-summation_wf bag-filter_wf list_wf nil_wf cons_wf monoid_p_wf comm_wf bag-no-repeats_wf bag_wf bool_wf decidable_wf filter_nil_lemma bag-summation-empty squash_wf true_wf bag-summation-zero iff_weakening_equal bag-summation-cons cons-bag_wf set_wf bag-member-cons infix_ap_wf list_ind_cons_lemma list_ind_nil_lemma bag-summation-add single-bag_wf bag-append_wf assoc_wf bag-filter-append bag-summation-append ifthenelse_wf bag-summation-filter bag-summation-single bag-extensionality-no-repeats subtype_rel_bag bag-filter-no-repeats bag-single-no-repeats bag-member-single bag-member-filter and_wf assert_elim subtype_base_sq bool_subtype_base
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 setEquality cumulativity sqequalRule lambdaEquality productEquality applyEquality functionExtensionality setElimination rename functionEquality because_Cache independent_isectElimination lambdaFormation independent_pairFormation independent_functionElimination voidEquality voidElimination dependent_functionElimination isect_memberEquality axiomEquality equalityTransitivity natural_numberEquality universeEquality imageMemberEquality baseClosed dependent_set_memberEquality inrFormation inlFormation instantiate

Latex:
\mforall{}[A:Type]
    \mforall{}[R,T:Type].  \mforall{}[add:R  {}\mrightarrow{}  R  {}\mrightarrow{}  R].  \mforall{}[zero:R].  \mforall{}[b:bag(T)].  \mforall{}[case:T  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:T  {}\mrightarrow{}  R].
    \mforall{}[c:bag(A)].
        \mSigma{}(x\mmember{}b).  f[x]  =  \mSigma{}(z\mmember{}c).  \mSigma{}(x\mmember{}[x\mmember{}b|case[x;z]]).  f[x] 
        supposing  (IsMonoid(R;add;zero)  \mwedge{}  Comm(R;add))
        \mwedge{}  (\mforall{}x:\{x:T|  x  \mdownarrow{}\mmember{}  b\}  .  (\mexists{}z:\{A|  (z  \mdownarrow{}\mmember{}  c  \mwedge{}  (\muparrow{}case[x;z]))\}))
        \mwedge{}  bag-no-repeats(A;c)
        \mwedge{}  (\mforall{}z1,z2:A.  \mforall{}x:T.    ((\muparrow{}case[x;z1])  {}\mRightarrow{}  (\muparrow{}case[x;z2])  {}\mRightarrow{}  (z1  =  z2))) 
    supposing  \mforall{}x,y:A.    Dec(x  =  y)



Date html generated: 2017_10_01-AM-09_02_30
Last ObjectModification: 2017_07_26-PM-04_43_33

Theory : bags


Home Index