Nuprl Lemma : bag_size_cons_lemma

b,x:Top.  (#(x.b) #(b) 1)


Proof




Definitions occuring in Statement :  bag-size: #(bs) cons-bag: x.b top: Top all: x:A. B[x] add: m natural_number: $n sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T cons-bag: x.b bag-size: #(bs) top: Top
Lemmas referenced :  top_wf length_of_cons_lemma
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut hypothesis lemma_by_obid sqequalRule sqequalHypSubstitution dependent_functionElimination thin isect_memberEquality voidElimination voidEquality

Latex:
\mforall{}b,x:Top.    (\#(x.b)  \msim{}  \#(b)  +  1)



Date html generated: 2016_05_15-PM-02_24_56
Last ObjectModification: 2015_12_27-AM-09_53_21

Theory : bags


Home Index