Nuprl Lemma : bag-map-cons

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


Proof




Definitions occuring in Statement :  bag-map: bag-map(f;bs) cons-bag: x.b uall: [x:A]. B[x] top: Top apply: a sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T bag-map: bag-map(f;bs) cons-bag: x.b all: x:A. B[x] top: Top
Lemmas referenced :  map_cons_lemma top_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality hypothesis sqequalAxiom isectElimination hypothesisEquality because_Cache

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



Date html generated: 2016_05_15-PM-02_25_41
Last ObjectModification: 2015_12_27-AM-09_52_47

Theory : bags


Home Index