### Nuprl Lemma : bag-count_wf

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  ((#x in bs) ∈ ℕ)`

Proof

Definitions occuring in Statement :  bag-count: `(#x in bs)` bag: `bag(T)` deq: `EqDecider(T)` nat: `ℕ` uall: `∀[x:A]. B[x]` member: `t ∈ T` universe: `Type`
Definitions unfolded in proof :  bag: `bag(T)` member: `t ∈ T` quotient: `x,y:A//B[x; y]` and: `P ∧ Q` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` bag-count: `(#x in bs)` so_lambda: `λ2x.t[x]` deq: `EqDecider(T)` so_apply: `x[s]` uimplies: `b supposing a` nat: `ℕ` sq_type: `SQType(T)` guard: `{T}` prop: `ℙ` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` subtype_rel: `A ⊆r B` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` not: `¬A` top: `Top` squash: `↓T` true: `True` ge: `i ≥ j ` count: `count(P;L)` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` eqof: `eqof(d)` ifthenelse: `if b then t else f fi ` le: `A ≤ B` less_than': `less_than'(a;b)` bfalse: `ff` bnot: `¬bb` assert: `↑b`
Lemmas referenced :  nat_wf list_wf permutation-invariant equal_wf count_wf subtype_base_sq set_subtype_base le_wf int_subtype_base cons_wf decidable__equal_int satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf intformimplies_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_formual_prop_imp_lemma iff_weakening_equal int_formula_prop_wf decidable__le nat_properties intformle_wf itermConstant_wf int_formula_prop_le_lemma int_term_value_constant_lemma permutation_wf equal-wf-base bag_wf deq_wf count-append nil_wf count-single reduce_cons_lemma bool_wf eqtt_to_assert safe-assert-deq itermAdd_wf int_term_value_add_lemma add_nat_wf false_wf add-is-int-iff eqff_to_assert bool_cases_sqequal bool_subtype_base assert-bnot ifthenelse_wf
Rules used in proof :  sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity pointwiseFunctionalityForEquality cut introduction extract_by_obid hypothesis sqequalRule pertypeElimination productElimination thin equalityTransitivity equalitySymmetry isectElimination cumulativity hypothesisEquality lambdaFormation because_Cache rename lambdaEquality applyEquality setElimination independent_functionElimination instantiate independent_isectElimination intEquality natural_numberEquality dependent_functionElimination unionElimination dependent_pairFormation int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation imageElimination equalityUniverse levelHypothesis imageMemberEquality baseClosed universeEquality computeAll dependent_set_memberEquality applyLambdaEquality productEquality isect_memberFormation axiomEquality equalityElimination addEquality pointwiseFunctionality promote_hyp baseApply closedConclusion

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].    ((\#x  in  bs)  \mmember{}  \mBbbN{})

Date html generated: 2018_05_21-PM-09_45_48
Last ObjectModification: 2017_07_26-PM-06_29_52

Theory : bags_2

Home Index