### Nuprl Lemma : filter_is_empty

`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  uiff(↑null(filter(P;L));∀[i:ℕ||L||]. (¬↑(P L[i])))`

Proof

Definitions occuring in Statement :  select: `L[n]` length: `||as||` null: `null(as)` filter: `filter(P;l)` list: `T List` int_seg: `{i..j-}` assert: `↑b` bool: `𝔹` uiff: `uiff(P;Q)` uall: `∀[x:A]. B[x]` not: `¬A` apply: `f a` function: `x:A ⟶ B[x]` natural_number: `\$n` universe: `Type`
Definitions unfolded in proof :  member: `t ∈ T` uall: `∀[x:A]. B[x]` int_seg: `{i..j-}` uimplies: `b supposing a` guard: `{T}` lelt: `i ≤ j < k` and: `P ∧ Q` all: `∀x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` not: `¬A` implies: `P `` Q` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` false: `False` top: `Top` prop: `ℙ` less_than: `a < b` squash: `↓T` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uiff: `uiff(P;Q)` assert: `↑b` ifthenelse: `if b then t else f fi ` btrue: `tt` bfalse: `ff` true: `True` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` bool: `𝔹` unit: `Unit` it: `⋅` l_all: `(∀x∈L.P[x])`
Lemmas referenced :  assert_wf select_wf int_seg_properties length_wf decidable__le full-omega-unsat 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 null_wf filter_wf5 subtype_rel_dep_function bool_wf l_member_wf subtype_rel_self set_wf uall_wf not_wf list_wf assert_witness null_cons_lemma false_wf true_wf l_all_wf equal-wf-T-base bnot_wf list_induction iff_wf filter_nil_lemma null_nil_lemma l_all_nil l_all_wf_nil filter_cons_lemma eqtt_to_assert uiff_transitivity eqff_to_assert assert_of_bnot equal_wf l_all_cons ifthenelse_wf cons_wf satisfiable-full-omega-tt
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity introduction extract_by_obid sqequalHypSubstitution isectElimination thin applyEquality functionExtensionality hypothesisEquality cumulativity because_Cache setElimination rename hypothesis independent_isectElimination natural_numberEquality productElimination dependent_functionElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation imageElimination setEquality lambdaFormation functionEquality universeEquality isect_memberFormation independent_pairEquality equalityTransitivity equalitySymmetry productEquality baseClosed equalityElimination computeAll

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].    uiff(\muparrow{}null(filter(P;L));\mforall{}[i:\mBbbN{}||L||].  (\mneg{}\muparrow{}(P  L[i])))

Date html generated: 2019_06_20-PM-01_25_50
Last ObjectModification: 2018_09_17-PM-10_26_04

Theory : list_1

Home Index