### Nuprl Lemma : sub-bag-of-bag-rep

`∀[T:Type]. ∀x:T. ∀n:ℕ.  ∀[b:bag(T)]. b = bag-rep(#(b);x) ∈ bag(T) supposing sub-bag(T;b;bag-rep(n;x))`

Proof

Definitions occuring in Statement :  sub-bag: `sub-bag(T;as;bs)` bag-rep: `bag-rep(n;x)` bag-size: `#(bs)` bag: `bag(T)` nat: `ℕ` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` all: `∀x:A. B[x]` uimplies: `b supposing a` single-valued-bag: `single-valued-bag(b;T)` implies: `P `` Q` subtype_rel: `A ⊆r B` prop: `ℙ` nat: `ℕ` decidable: `Dec(P)` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bag-rep: `bag-rep(n;x)` top: `Top` ge: `i ≥ j ` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` and: `P ∧ Q` squash: `↓T` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  iff_weakening_equal true_wf squash_wf sv-bag-only_wf int_formula_prop_less_lemma intformless_wf le_wf decidable__lt bag-member-sv-bag-only single-valued-bag-is-rep empty-bag_wf int_formula_prop_wf int_formula_prop_eq_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma intformeq_wf itermConstant_wf itermVar_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties bag-size-zero primrec0_lemma int_subtype_base subtype_base_sq bag_wf sub-bag_wf nat_wf bag-size_wf decidable__equal_int bag-member_wf member-bag-rep list-subtype-bag bag-rep_wf sub-bag-member
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lambdaFormation lemma_by_obid sqequalHypSubstitution isectElimination thin because_Cache hypothesisEquality hypothesis applyEquality independent_isectElimination lambdaEquality sqequalRule equalityTransitivity equalitySymmetry dependent_functionElimination setElimination rename natural_numberEquality unionElimination isect_memberEquality axiomEquality universeEquality instantiate cumulativity intEquality independent_functionElimination voidElimination voidEquality dependent_pairFormation int_eqEquality independent_pairFormation computeAll setEquality imageElimination imageMemberEquality baseClosed productElimination

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}n:\mBbbN{}.    \mforall{}[b:bag(T)].  b  =  bag-rep(\#(b);x)  supposing  sub-bag(T;b;bag-rep(n;x))

Date html generated: 2016_05_15-PM-02_46_28
Last ObjectModification: 2016_01_16-AM-08_44_01

Theory : bags

Home Index