Nuprl Lemma : bag_null_empty_lemma
bag-null({}) ~ tt
Proof
Definitions occuring in Statement :
bag-null: bag-null(bs),
empty-bag: {},
btrue: tt,
sqequal: s ~ t
Definitions unfolded in proof :
empty-bag: {},
bag-null: bag-null(bs)
Lemmas referenced :
null_nil_lemma
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
cut,
lemma_by_obid,
hypothesis
Latex:
bag-null(\{\}) \msim{} tt
Date html generated:
2016_05_15-PM-02_23_55
Last ObjectModification:
2015_12_27-AM-09_53_38
Theory : bags
Home
Index