### Nuprl Lemma : bag-moebius-no-repeats

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[b:bag(T)].`
`  bag-moebius(eq;b) ~ if (#(b) rem 2 =z 0) then 1 else -1 fi  supposing ↑bag-has-no-repeats(eq;b)`

Proof

Definitions occuring in Statement :  bag-moebius: `bag-moebius(eq;b)` bag-has-no-repeats: `bag-has-no-repeats(eq;b)` bag-size: `#(bs)` bag: `bag(T)` deq: `EqDecider(T)` assert: `↑b` ifthenelse: `if b then t else f fi ` eq_int: `(i =z j)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` remainder: `n rem m` minus: `-n` natural_number: `\$n` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` bag-moebius: `bag-moebius(eq;b)` all: `∀x:A. B[x]` implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` true: `True` nequal: `a ≠ b ∈ T ` not: `¬A` sq_type: `SQType(T)` guard: `{T}` false: `False` prop: `ℙ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` bnot: `¬bb` assert: `↑b`
Lemmas referenced :  subtype_base_sq int_subtype_base bag-has-no-repeats_wf bool_wf eqtt_to_assert eq_int_wf equal-wf-base true_wf assert_of_eq_int eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_int assert_wf bag_wf deq_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin instantiate extract_by_obid sqequalHypSubstitution isectElimination cumulativity intEquality independent_isectElimination hypothesis hypothesisEquality lambdaFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination sqequalRule remainderEquality because_Cache natural_numberEquality addLevel dependent_functionElimination independent_functionElimination voidElimination baseClosed dependent_pairFormation promote_hyp minusEquality sqequalAxiom isect_memberEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[b:bag(T)].
bag-moebius(eq;b)  \msim{}  if  (\#(b)  rem  2  =\msubz{}  0)  then  1  else  -1  fi    supposing  \muparrow{}bag-has-no-repeats(eq;b)

Date html generated: 2018_05_21-PM-09_53_42
Last ObjectModification: 2017_07_26-PM-06_32_24

Theory : bags_2

Home Index