### Nuprl Lemma : bag-member-count

`∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  uiff(x ↓∈ bs;1 ≤ (#x in bs))`

Proof

Definitions occuring in Statement :  bag-count: `(#x in bs)` bag-member: `x ↓∈ bs` bag: `bag(T)` deq: `EqDecider(T)` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` le: `A ≤ B` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` uimplies: `b supposing a` le: `A ≤ B` not: `¬A` implies: `P `` Q` false: `False` deq: `EqDecider(T)` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` bag-member: `x ↓∈ bs` squash: `↓T` nat: `ℕ` sq_stable: `SqStable(P)` exists: `∃x:A. B[x]` bag-filter: `[x∈b|p[x]]` bag-size: `#(bs)` all: `∀x:A. B[x]` or: `P ∨ Q` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` true: `True` l_member: `(x ∈ l)` int_seg: `{i..j-}` lelt: `i ≤ j < k` eqof: `eqof(d)` ge: `i ≥ j ` cand: `A c∧ B` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` top: `Top` rev_uimplies: `rev_uimplies(P;Q)` cons: `[a / b]` bfalse: `ff` guard: `{T}` less_than: `a < b` bag: `bag(T)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` quotient: `x,y:A//B[x; y]` less_than': `less_than'(a;b)` sq_type: `SQType(T)`
Lemmas referenced :  bag-count-sqequal less_than'_wf bag-size_wf assert_wf bag-filter_wf bag-member_wf le_wf bag-count_wf nat_wf bag_wf deq_wf sq_stable__le filter_is_empty filter_wf5 l_member_wf list_wf list-cases null_nil_lemma length_of_nil_lemma lelt_wf length_wf safe-assert-deq select_wf nat_properties decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_le_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf product_subtype_list null_cons_lemma length_of_cons_lemma non_neg_length itermAdd_wf int_term_value_add_lemma uiff_wf null_wf3 subtype_rel_list top_wf uall_wf int_seg_wf not_wf int_seg_properties decidable__lt intformless_wf int_formula_prop_less_lemma equal_wf permutation_wf permutation_weakening quotient-member-eq permutation-equiv list-subtype-bag equal-wf-base member_wf squash_wf true_wf decidable__exists_int_seg decidable__assert int_seg_subtype_nat false_wf less_than_wf subtype_base_sq set_subtype_base int_subtype_base decidable__equal_int intformeq_wf int_formula_prop_eq_lemma
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity cut introduction extract_by_obid sqequalHypSubstitution sqequalTransitivity computationStep isectElimination thin because_Cache hypothesisEquality hypothesis independent_pairFormation isect_memberFormation productElimination independent_pairEquality lambdaEquality dependent_functionElimination voidElimination setEquality cumulativity applyEquality setElimination rename natural_numberEquality axiomEquality equalityTransitivity equalitySymmetry imageElimination imageMemberEquality baseClosed universeEquality isect_memberEquality independent_functionElimination hyp_replacement applyLambdaEquality lambdaFormation unionElimination independent_isectElimination dependent_set_memberEquality dependent_pairFormation int_eqEquality intEquality voidEquality computeAll promote_hyp hypothesis_subsumption functionEquality instantiate pointwiseFunctionality pertypeElimination productEquality

Latex:
\mforall{}[T:Type].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].    uiff(x  \mdownarrow{}\mmember{}  bs;1  \mleq{}  (\#x  in  bs))

Date html generated: 2018_05_21-PM-09_46_00
Last ObjectModification: 2017_07_26-PM-06_29_54

Theory : bags_2

Home Index