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))))


Definitions occuring in Statement :  last: last(L) null: null(as) filter: filter(P;l) list: List assert: b bool: 𝔹 uimplies: supposing a uall: [x:A]. B[x] not: ¬A apply: a function: x:A ⟶ B[x] universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] uimplies: supposing a not: ¬A implies:  Q member: t ∈ T uiff: uiff(P;Q) and: P ∧ Q assert: b ifthenelse: if then else 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 ⊆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

\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