### Nuprl Lemma : hd-filter

`∀[T:Type]`
`  ∀P:T ⟶ 𝔹. ∀as:T List.`
`    ((∃a:T. ((a ∈ as) ∧ (↑P[a])))`
`    `` ((hd(filter(λa.P[a];as)) ∈ T) c∧ ((hd(filter(λa.P[a];as)) ∈ as) ∧ (↑P[hd(filter(λa.P[a];as))]))))`

Proof

Definitions occuring in Statement :  l_member: `(x ∈ l)` hd: `hd(l)` filter: `filter(P;l)` list: `T List` assert: `↑b` bool: `𝔹` uall: `∀[x:A]. B[x]` cand: `A c∧ B` so_apply: `x[s]` all: `∀x:A. B[x]` exists: `∃x:A. B[x]` implies: `P `` Q` and: `P ∧ Q` member: `t ∈ T` lambda: `λx.A[x]` function: `x:A ⟶ B[x]` universe: `Type`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` implies: `P `` Q` member: `t ∈ T` so_apply: `x[s]` uimplies: `b supposing a` so_lambda: `λ2x.t[x]` prop: `ℙ` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` cand: `A c∧ B` subtype_rel: `A ⊆r B` ge: `i ≥ j ` exists: `∃x:A. B[x]` decidable: `Dec(P)` or: `P ∨ Q` less_than: `a < b` squash: `↓T` satisfiable_int_formula: `satisfiable_int_formula(fmla)` false: `False` not: `¬A` top: `Top` less_than': `less_than'(a;b)` length: `||as||` list_ind: list_ind nil: `[]` it: `⋅` cons: `[a / b]` sq_stable: `SqStable(P)`
Lemmas referenced :  filter_type length-filter-pos l_exists_iff l_member_wf assert_wf exists_wf list_wf bool_wf hd_wf subtype_rel_list decidable__le length_wf satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermVar_wf intformless_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_less_lemma int_formula_prop_wf less_than_wf equal_wf hd_member set_wf list-cases product_subtype_list assert_elim null_wf3 top_wf null_cons_lemma bfalse_wf btrue_neq_bfalse member_filter sq_stable__assert
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality lambdaEquality applyEquality functionExtensionality cumulativity because_Cache independent_isectElimination dependent_functionElimination sqequalRule hypothesis setElimination rename setEquality productElimination independent_functionElimination productEquality functionEquality universeEquality equalityTransitivity equalitySymmetry natural_numberEquality unionElimination imageElimination dependent_pairFormation int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll promote_hyp hypothesis_subsumption addLevel levelHypothesis hyp_replacement applyLambdaEquality imageMemberEquality baseClosed

Latex:
\mforall{}[T:Type]
\mforall{}P:T  {}\mrightarrow{}  \mBbbB{}.  \mforall{}as:T  List.
((\mexists{}a:T.  ((a  \mmember{}  as)  \mwedge{}  (\muparrow{}P[a])))
{}\mRightarrow{}  ((hd(filter(\mlambda{}a.P[a];as))  \mmember{}  T)
c\mwedge{}  ((hd(filter(\mlambda{}a.P[a];as))  \mmember{}  as)  \mwedge{}  (\muparrow{}P[hd(filter(\mlambda{}a.P[a];as))]))))

Date html generated: 2018_05_21-PM-06_50_26
Last ObjectModification: 2017_07_26-PM-04_57_29

Theory : general

Home Index