Nuprl Lemma : bag-moebius-no-repeats

[T:Type]. ∀[eq:EqDecider(T)]. ∀[b:bag(T)].
  bag-moebius(eq;b) if (#(b) rem =z 0) then 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 then else fi  eq_int: (i =z j) uimplies: supposing a uall: [x:A]. B[x] remainder: rem m minus: -n natural_number: $n universe: Type sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a bag-moebius: bag-moebius(eq;b) 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  true: True nequal: a ≠ b ∈  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