### Nuprl Lemma : bag-count-filter

`∀[T:Type]. ∀[p:T ⟶ 𝔹]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[bs:bag(T)].  ((#x in [t∈bs|p[t]]) ≤ (#x in bs))`

Proof

Definitions occuring in Statement :  bag-count: `(#x in bs)` bag-filter: `[x∈b|p[x]]` bag: `bag(T)` deq: `EqDecider(T)` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` le: `A ≤ B` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` sq_stable: `SqStable(P)` implies: `P `` Q` squash: `↓T` so_lambda: `λ2x.t[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` prop: `ℙ` uimplies: `b supposing a` all: `∀x:A. B[x]` nat: `ℕ` exists: `∃x:A. B[x]` bag-filter: `[x∈b|p[x]]` bag-size: `#(bs)` top: `Top` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` band: `p ∧b q` ifthenelse: `if b then t else f fi ` uiff: `uiff(P;Q)` and: `P ∧ Q` deq: `EqDecider(T)` bfalse: `ff` l_all: `(∀x∈L.P[x])` int_seg: `{i..j-}` guard: `{T}` lelt: `i ≤ j < k` decidable: `Dec(P)` or: `P ∨ Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` less_than: `a < b` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` eqof: `eqof(d)`
Lemmas referenced :  sq_stable__le bag_wf deq_wf bool_wf bag-filter_wf subtype_rel_bag assert_wf bag-count_wf nat_wf equal_wf bag_to_squash_list le_wf list-subtype-bag bag-count-sqequal filter-filter length-filter-le eqtt_to_assert select_wf int_seg_properties length_wf 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 decidable__lt intformless_wf int_formula_prop_less_lemma int_seg_wf band_wf eqof_wf l_member_wf l_all_wf2 l_all_functionality iff_transitivity iff_weakening_uiff assert_of_band safe-assert-deq
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis independent_functionElimination sqequalRule imageMemberEquality hypothesisEquality baseClosed imageElimination cumulativity functionEquality universeEquality lambdaEquality applyEquality functionExtensionality setEquality independent_isectElimination setElimination rename because_Cache lambdaFormation equalityTransitivity equalitySymmetry dependent_functionElimination productElimination promote_hyp hyp_replacement applyLambdaEquality isect_memberEquality voidElimination voidEquality unionElimination equalityElimination productEquality natural_numberEquality dependent_pairFormation int_eqEquality intEquality independent_pairFormation computeAll addLevel impliesFunctionality

Latex:
\mforall{}[T:Type].  \mforall{}[p:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[eq:EqDecider(T)].  \mforall{}[x:T].  \mforall{}[bs:bag(T)].
((\#x  in  [t\mmember{}bs|p[t]])  \mleq{}  (\#x  in  bs))

Date html generated: 2018_05_21-PM-09_46_09
Last ObjectModification: 2017_07_26-PM-06_29_57

Theory : bags_2

Home Index