### Nuprl Lemma : count-bag-to-set

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[bs:bag(T)]. ∀[x:T].  ((#x in bag-to-set(eq;bs)) ~ if 0 <z (#x in bs) then 1 else 0 fi )`

Proof

Definitions occuring in Statement :  bag-to-set: `bag-to-set(eq;bs)` bag-count: `(#x in bs)` bag: `bag(T)` deq: `EqDecider(T)` ifthenelse: `if b then t else f fi ` lt_int: `i <z j` uall: `∀[x:A]. B[x]` natural_number: `\$n` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  bag-to-set: `bag-to-set(eq;bs)`
Lemmas referenced :  count-bag-remove-repeats
Rules used in proof :  cut lemma_by_obid sqequalHypSubstitution sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep hypothesis

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[bs:bag(T)].  \mforall{}[x:T].
((\#x  in  bag-to-set(eq;bs))  \msim{}  if  0  <z  (\#x  in  bs)  then  1  else  0  fi  )

Date html generated: 2016_05_15-PM-08_03_01
Last ObjectModification: 2015_12_27-PM-04_15_31

Theory : bags_2

Home Index