### Nuprl Lemma : length-filter-decreases

`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  ((∃x∈L. ¬↑(P x)) `` ||filter(P;L)|| < ||L||)`

Proof

Definitions occuring in Statement :  l_exists: `(∃x∈L. P[x])` length: `||as||` filter: `filter(P;l)` list: `T List` assert: `↑b` bool: `𝔹` less_than: `a < b` uall: `∀[x:A]. B[x]` not: `¬A` implies: `P `` Q` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` implies: `P `` Q` prop: `ℙ` all: `∀x:A. B[x]` so_apply: `x[s]` subtype_rel: `A ⊆r B` uimplies: `b supposing a` top: `Top` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` and: `P ∧ Q` ifthenelse: `if b then t else f fi ` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` l_exists: `(∃x∈L. P[x])` int_seg: `{i..j-}` lelt: `i ≤ j < k` decidable: `Dec(P)` satisfiable_int_formula: `satisfiable_int_formula(fmla)` not: `¬A` less_than: `a < b` squash: `↓T` select: `L[n]` cons: `[a / b]` ge: `i ≥ j ` le: `A ≤ B`
Lemmas referenced :  list_induction l_exists_wf l_member_wf not_wf assert_wf less_than_wf length_wf filter_wf5 subtype_rel_dep_function bool_wf subtype_rel_self set_wf list_wf filter_nil_lemma length_of_nil_lemma l_exists_wf_nil filter_cons_lemma length_of_cons_lemma eqtt_to_assert eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot member-less_than int_seg_properties decidable__lt satisfiable-full-omega-tt intformand_wf intformless_wf itermVar_wf itermConstant_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_wf intformnot_wf itermAdd_wf int_formula_prop_not_lemma int_term_value_add_lemma decidable__equal_int int_subtype_base select-cons-tl intformeq_wf int_formula_prop_eq_lemma subtract_wf decidable__le itermSubtract_wf int_term_value_subtract_lemma non_neg_length lelt_wf select_wf length-filter
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality cumulativity lambdaFormation hypothesis setElimination rename applyEquality functionExtensionality because_Cache setEquality independent_isectElimination independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality unionElimination equalityElimination equalityTransitivity equalitySymmetry productElimination dependent_pairFormation promote_hyp instantiate universeEquality natural_numberEquality int_eqEquality intEquality independent_pairFormation computeAll addEquality imageElimination dependent_set_memberEquality

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].    ((\mexists{}x\mmember{}L.  \mneg{}\muparrow{}(P  x))  {}\mRightarrow{}  ||filter(P;L)||  <  ||L||)

Date html generated: 2017_04_17-AM-07_51_29
Last ObjectModification: 2017_02_27-PM-04_25_51

Theory : list_1

Home Index