### Nuprl Lemma : bag-null-rep

`∀[n:ℕ]. ∀[x:Top].  (bag-null(bag-rep(n;x)) ~ (n =z 0))`

Proof

Definitions occuring in Statement :  bag-rep: `bag-rep(n;x)` bag-null: `bag-null(bs)` nat: `ℕ` eq_int: `(i =z j)` uall: `∀[x:A]. B[x]` top: `Top` natural_number: `\$n` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` subtype_rel: `A ⊆r B` nat: `ℕ` uimplies: `b supposing a` top: `Top` sq_type: `SQType(T)` implies: `P `` Q` guard: `{T}`
Lemmas referenced :  bag-null_wf top_wf bag-rep_wf eq_int_wf subtype_base_sq bool_subtype_base null-bag-size list-subtype-bag bag-size-rep nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesis isectElimination hypothesisEquality applyEquality because_Cache sqequalRule setElimination rename natural_numberEquality instantiate independent_isectElimination lambdaEquality isect_memberEquality voidElimination voidEquality equalityTransitivity equalitySymmetry independent_functionElimination sqequalAxiom

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:Top].    (bag-null(bag-rep(n;x))  \msim{}  (n  =\msubz{}  0))

Date html generated: 2016_05_15-PM-02_34_09
Last ObjectModification: 2015_12_27-AM-09_46_45

Theory : bags

Home Index