Nuprl Lemma : filter-length-less

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


Proof




Definitions occuring in Statement :  l_member: (x ∈ l) length: ||as|| filter: filter(P;l) list: List assert: b bool: 𝔹 less_than: a < b uimplies: supposing a uall: [x:A]. B[x] so_apply: x[s] exists: x:A. B[x] not: ¬A and: P ∧ Q lambda: λx.A[x] function: x:A ⟶ B[x] universe: Type
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a exists: x:A. B[x] and: P ∧ Q all: x:A. B[x] so_apply: x[s] prop: iff: ⇐⇒ Q rev_implies:  Q implies:  Q cand: c∧ B uiff: uiff(P;Q) rev_uimplies: rev_uimplies(P;Q) decidable: Dec(P) or: P ∨ Q less_than: a < b squash: T false: False not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) top: Top
Lemmas referenced :  filter-split-length member_filter_2 bnot_wf l_member_wf assert_of_bnot l_member_length filter_wf5 decidable__lt length_wf add-is-int-iff full-omega-unsat intformand_wf intformnot_wf intformless_wf itermVar_wf itermConstant_wf intformeq_wf itermAdd_wf istype-int int_formula_prop_and_lemma istype-void int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_eq_lemma int_term_value_add_lemma int_formula_prop_wf false_wf istype-assert list_wf bool_wf istype-universe
Rules used in proof :  cut introduction extract_by_obid sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation_alt hypothesis sqequalHypSubstitution isectElimination thin hypothesisEquality productElimination dependent_functionElimination lambdaEquality_alt applyEquality setElimination rename setIsType inhabitedIsType universeIsType independent_functionElimination sqequalRule independent_pairFormation independent_isectElimination equalityTransitivity equalitySymmetry unionElimination imageElimination pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed natural_numberEquality approximateComputation dependent_pairFormation_alt int_eqEquality isect_memberEquality_alt voidElimination productIsType functionIsType instantiate universeEquality

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



Date html generated: 2020_05_19-PM-09_42_47
Last ObjectModification: 2019_10_29-AM-10_00_34

Theory : list_1


Home Index