Nuprl Lemma : bag-map-append-empty

[f,b:Top].  (bag-map(f;b) {} bag-map(f;b))


Proof




Definitions occuring in Statement :  bag-append: as bs bag-map: bag-map(f;bs) empty-bag: {} uall: [x:A]. B[x] top: Top sqequal: t
Definitions unfolded in proof :  bag-map: bag-map(f;bs) empty-bag: {} bag-append: as bs uall: [x:A]. B[x] member: t ∈ T
Lemmas referenced :  map-append-empty top_wf
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis sqequalAxiom isect_memberEquality because_Cache

Latex:
\mforall{}[f,b:Top].    (bag-map(f;b)  +  \{\}  \msim{}  bag-map(f;b))



Date html generated: 2016_05_15-PM-03_08_43
Last ObjectModification: 2015_12_27-AM-09_26_25

Theory : bags


Home Index