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 <(#x in bs) then else 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 then else fi  lt_int: i <j uall: [x:A]. B[x] natural_number: $n universe: Type sqequal: 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