### Nuprl Lemma : last-filter1

`∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List].`
`  (last(filter(P;L)) = last(L) ∈ A) supposing ((↑(P last(L))) and (¬↑null(filter(P;L))))`

Proof

Definitions occuring in Statement :  last: `last(L)` null: `null(as)` filter: `filter(P;l)` list: `T List` assert: `↑b` bool: `𝔹` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` apply: `f a` function: `x:A ⟶ B[x]` universe: `Type` equal: `s = t ∈ T`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` uimplies: `b supposing a` not: `¬A` implies: `P `` Q` member: `t ∈ T` uiff: `uiff(P;Q)` and: `P ∧ Q` assert: `↑b` ifthenelse: `if b then t else f fi ` null: `null(as)` filter: `filter(P;l)` reduce: `reduce(f;k;as)` list_ind: list_ind nil: `[]` it: `⋅` btrue: `tt` true: `True` prop: `ℙ` subtype_rel: `A ⊆r B` so_lambda: `λ2x.t[x]` so_apply: `x[s]` all: `∀x:A. B[x]` false: `False` top: `Top` bfalse: `ff` bool: `𝔹` unit: `Unit` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb`
Lemmas referenced :  assert_of_null assert_wf null_wf filter_wf5 subtype_rel_dep_function bool_wf l_member_wf subtype_rel_self set_wf list_induction not_wf last_wf equal_wf null_nil_lemma filter_nil_lemma true_wf null_cons_lemma filter_cons_lemma eqtt_to_assert eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot list_wf subtype_rel_list top_wf member-implies-null-eq-bfalse and_wf btrue_neq_bfalse equal-wf-T-base btrue_wf false_wf last_cons2 null-filter2 last_member l_all_fwd
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation cut lambdaFormation introduction sqequalHypSubstitution independent_functionElimination thin extract_by_obid isectElimination hypothesisEquality hypothesis productElimination independent_isectElimination natural_numberEquality hyp_replacement equalitySymmetry applyLambdaEquality cumulativity applyEquality sqequalRule lambdaEquality setEquality setElimination rename because_Cache voidElimination promote_hyp functionEquality functionExtensionality dependent_functionElimination isect_memberEquality voidEquality unionElimination equalityElimination equalityTransitivity dependent_pairFormation instantiate universeEquality dependent_set_memberEquality independent_pairFormation baseClosed addLevel impliesFunctionality

Latex:
\mforall{}[A:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:A  List].
(last(filter(P;L))  =  last(L))  supposing  ((\muparrow{}(P  last(L)))  and  (\mneg{}\muparrow{}null(filter(P;L))))

Date html generated: 2017_04_17-AM-07_52_55
Last ObjectModification: 2017_02_27-PM-04_26_08

Theory : list_1

Home Index