Nuprl Lemma : bag_size_empty_lemma
#({}) ~ 0
Proof
Definitions occuring in Statement :
bag-size: #(bs),
empty-bag: {},
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
empty-bag: {},
bag-size: #(bs)
Lemmas referenced :
length_of_nil_lemma
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
hypothesis
Latex:
\#(\{\}) \msim{} 0
Date html generated:
2016_05_15-PM-02_25_08
Last ObjectModification:
2015_12_27-AM-09_53_12
Theory : bags
Home
Index