### Nuprl Lemma : decidable-filter

`∀[T:Type]`
`  ∀L:T List`
`    ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ]. ((∀x∈L.Dec(P[x])) `` (∃L':T List. (L' ⊆ L ∧ (∀x:T. ((x ∈ L') `⇐⇒` (x ∈ L) ∧ P[x])))))`

Proof

Definitions occuring in Statement :  sublist: `L1 ⊆ L2` l_all: `(∀x∈L.P[x])` l_member: `(x ∈ l)` list: `T List` decidable: `Dec(P)` uall: `∀[x:A]. B[x]` prop: `ℙ` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` iff: `P `⇐⇒` Q` implies: `P `` Q` and: `P ∧ Q` set: `{x:A| B[x]} ` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` prop: `ℙ` implies: `P `` Q` so_apply: `x[s]` subtype_rel: `A ⊆r B` and: `P ∧ Q` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` exists: `∃x:A. B[x]` cand: `A c∧ B` top: `Top` uimplies: `b supposing a` not: `¬A` false: `False` decidable: `Dec(P)` or: `P ∨ Q` guard: `{T}` cons: `[a / b]` true: `True` sublist: `L1 ⊆ L2` int_seg: `{i..j-}` lelt: `i ≤ j < k` satisfiable_int_formula: `satisfiable_int_formula(fmla)` less_than: `a < b` squash: `↓T` ge: `i ≥ j ` le: `A ≤ B` nat: `ℕ` l_member: `(x ∈ l)`
Lemmas referenced :  list_induction uall_wf l_all_wf l_member_wf decidable_wf exists_wf list_wf sublist_wf all_wf iff_wf l_all_wf_nil cons_wf nil_wf nil-sublist null_nil_lemma btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse l_all_cons cons_member cons_sublist_cons equal_wf and_wf list-cases product_subtype_list nil_sublist list-subtype subtype_rel_list int_seg_wf length_wf increasing_wf length_wf_nat select_wf int_seg_properties 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 non_neg_length lelt_wf nat_properties l_member-settype set_wf
Rules used in proof :  cut sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation thin instantiate introduction extract_by_obid sqequalHypSubstitution isectElimination cumulativity hypothesisEquality sqequalRule lambdaEquality functionEquality because_Cache universeEquality hypothesis setElimination rename applyEquality functionExtensionality setEquality productEquality independent_functionElimination voidElimination voidEquality dependent_functionElimination dependent_pairFormation isect_memberEquality independent_pairFormation independent_isectElimination equalityTransitivity equalitySymmetry productElimination unionElimination inlFormation inrFormation hyp_replacement dependent_set_memberEquality applyLambdaEquality promote_hyp hypothesis_subsumption natural_numberEquality addLevel levelHypothesis int_eqEquality intEquality computeAll imageElimination

Latex:
\mforall{}[T:Type]
\mforall{}L:T  List
\mforall{}[P:\{x:T|  (x  \mmember{}  L)\}    {}\mrightarrow{}  \mBbbP{}]
((\mforall{}x\mmember{}L.Dec(P[x]))  {}\mRightarrow{}  (\mexists{}L':T  List.  (L'  \msubseteq{}  L  \mwedge{}  (\mforall{}x:T.  ((x  \mmember{}  L')  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L)  \mwedge{}  P[x])))))

Date html generated: 2017_10_01-AM-09_13_07
Last ObjectModification: 2017_07_26-PM-04_48_38

Theory : general

Home Index