Nuprl Lemma : bag-moebius-property

[T:Type]
  ∀[eq:EqDecider(T)]. ∀[b:bag(T)].
    (bag-moebius(eq;b)
    if bag-null(b) then else (p∈[p∈bag-partitions(eq;b)|¬bbag-null(fst(p))]). bag-moebius(eq;snd(p)) fi 
    ∈ ℤ
  supposing valueall-type(T)


Proof




Definitions occuring in Statement :  bag-moebius: bag-moebius(eq;b) bag-partitions: bag-partitions(eq;bs) bag-summation: Σ(x∈b). f[x] bag-null: bag-null(bs) bag-filter: [x∈b|p[x]] bag: bag(T) deq: EqDecider(T) valueall-type: valueall-type(T) bnot: ¬bb ifthenelse: if then else fi  uimplies: supposing a uall: [x:A]. B[x] pi1: fst(t) pi2: snd(t) lambda: λx.A[x] add: m minus: -n natural_number: $n int: universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q ifthenelse: if then else fi  bfalse: ff exists: x:A. B[x] prop: or: P ∨ Q sq_type: SQType(T) guard: {T} bnot: ¬bb assert: b false: False not: ¬A bag-moebius: bag-moebius(eq;b) bag-has-no-repeats: bag-has-no-repeats(eq;b) eq_int: (i =z j) bag-size: #(bs) length: ||as|| list_ind: list_ind bag-remove-repeats: bag-remove-repeats(eq;bs) list-to-set: list-to-set(eq;L) l-union: as ⋃ bs reduce: reduce(f;k;as) empty-bag: {} nil: [] infix_ap: y decidable: Dec(P) satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top assoc: Assoc(T;op) comm: Comm(T;op) monoid_p: IsMonoid(T;op;id) ident: Ident(T;op;id) cand: c∧ B so_lambda: λ2x.t[x] subtype_rel: A ⊆B nat: so_apply: x[s] squash: T pi1: fst(t) pi2: snd(t) true: True iff: ⇐⇒ Q rev_implies:  Q bag-member: x ↓∈ bs sub-bag: sub-bag(T;as;bs) rev_uimplies: rev_uimplies(P;Q) inject: Inj(A;B;f) sq_stable: SqStable(P)
Lemmas referenced :  bag-null_wf bool_wf eqtt_to_assert assert-bag-null eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot equal-wf-T-base bag_wf deq_wf valueall-type_wf bag-moebius_wf bag-moebius-property1 decidable__equal_int satisfiable-full-omega-tt intformnot_wf intformeq_wf itermAdd_wf itermVar_wf int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_wf add-is-int-iff intformand_wf itermMinus_wf itermConstant_wf int_formula_prop_and_lemma int_term_value_minus_lemma int_term_value_constant_lemma false_wf int_subtype_base bag-summation-split sub-bags_wf eq_int_wf bag-size_wf nat_wf squash_wf true_wf bag-summation_wf assert_wf bnot_wf pi1_wf_top bag-filter_wf bag-partitions_wf iff_weakening_equal bag-summation-single bag-extensionality-no-repeats decidable__equal_bag decidable-equal-deq subtype_rel_bag single-bag_wf bag-single-no-repeats bag-member-single bag-member_wf bag-no-repeats-filter sub-bags-no-repeats bag-member-filter assert_of_eq_int member-sub-bags bag-size-append bag-size-is-zero bag-append-empty bag-subtype-list sub-bag_weakening bag-summation-map assoc_wf comm_wf bag-map_wf bag-map-no-repeats bag-append_wf pi2_wf bag-settype bag-member-partitions top_wf subtype_rel_product subtype_rel_self set_wf bag-append-comm bag-append-cancel no-repeats-bag-partitions bag-no-repeats-subtype strong-subtype-set2 bag-member-map sq_stable__bag-member bag-member-filter-set iff_transitivity not_wf iff_weakening_uiff assert_of_bnot null-bag-size
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut extract_by_obid sqequalHypSubstitution dependent_functionElimination thin cumulativity hypothesisEquality hypothesis lambdaFormation unionElimination equalityElimination isectElimination equalityTransitivity equalitySymmetry productElimination independent_isectElimination sqequalRule dependent_pairFormation promote_hyp instantiate because_Cache independent_functionElimination voidElimination baseClosed isect_memberEquality axiomEquality universeEquality natural_numberEquality hyp_replacement applyLambdaEquality intEquality lambdaEquality int_eqEquality voidEquality computeAll independent_pairFormation pointwiseFunctionality rename baseApply closedConclusion independent_pairEquality addEquality applyEquality setElimination imageElimination setEquality productEquality imageMemberEquality functionExtensionality functionEquality equalityUniverse levelHypothesis dependent_set_memberEquality impliesFunctionality

Latex:
\mforall{}[T:Type]
    \mforall{}[eq:EqDecider(T)].  \mforall{}[b:bag(T)].
        (bag-moebius(eq;b)
        =  if  bag-null(b)
            then  1
            else  -\mSigma{}(p\mmember{}[p\mmember{}bag-partitions(eq;b)|\mneg{}\msubb{}bag-null(fst(p))]).  bag-moebius(eq;snd(p))
            fi  ) 
    supposing  valueall-type(T)



Date html generated: 2018_05_21-PM-09_54_40
Last ObjectModification: 2017_07_26-PM-06_32_29

Theory : bags_2


Home Index