### Nuprl Lemma : length-filter-bnot

`∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹].  (||filter(λa.(¬bP[a]);L)|| = (||L|| - ||filter(λa.P[a];L)||) ∈ ℤ)`

Proof

Definitions occuring in Statement :  l_member: `(x ∈ l)` length: `||as||` filter: `filter(P;l)` list: `T List` bnot: `¬bb` bool: `𝔹` uall: `∀[x:A]. B[x]` so_apply: `x[s]` set: `{x:A| B[x]} ` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` subtract: `n - m` int: `ℤ` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` all: `∀x:A. B[x]` so_apply: `x[s]` implies: `P `` Q` top: `Top` subtract: `n - m` subtype_rel: `A ⊆r B` uimplies: `b supposing a` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` guard: `{T}` or: `P ∨ Q` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` bnot: `¬bb` ifthenelse: `if b then t else f fi ` bfalse: `ff` decidable: `Dec(P)` false: `False` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` not: `¬A` sq_type: `SQType(T)` assert: `↑b`
Lemmas referenced :  list_induction uall_wf l_member_wf bool_wf equal_wf length_wf filter_wf5 bnot_wf subtract_wf list_wf filter_nil_lemma length_of_nil_lemma nil_wf filter_cons_lemma length_of_cons_lemma subtype_rel_dep_function cons_wf subtype_rel_sets cons_member subtype_rel_self set_wf eqtt_to_assert decidable__equal_int subtract-is-int-iff satisfiable-full-omega-tt intformand_wf intformnot_wf intformeq_wf itermVar_wf itermSubtract_wf itermAdd_wf itermConstant_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_eq_lemma int_term_value_var_lemma int_term_value_subtract_lemma int_term_value_add_lemma int_term_value_constant_lemma int_formula_prop_wf false_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality sqequalRule lambdaEquality functionEquality setEquality cumulativity because_Cache hypothesis lambdaFormation setElimination rename intEquality applyEquality functionExtensionality dependent_set_memberEquality independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality natural_numberEquality independent_isectElimination productElimination inrFormation inlFormation unionElimination equalityElimination equalityTransitivity equalitySymmetry pointwiseFunctionality promote_hyp baseApply closedConclusion baseClosed dependent_pairFormation int_eqEquality independent_pairFormation computeAll instantiate axiomEquality universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbB{}].
(||filter(\mlambda{}a.(\mneg{}\msubb{}P[a]);L)||  =  (||L||  -  ||filter(\mlambda{}a.P[a];L)||))

Date html generated: 2017_04_17-AM-08_58_52
Last ObjectModification: 2017_02_27-PM-05_15_43

Theory : list_1

Home Index