Nuprl Lemma : last_index

Nuprl Lemma : last_index_property

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].

  ((↑P[L[last_index(L;x.P[x]) - 1]]) ∧ (¬(∃x∈nth_tl(last_index(L;x.P[x]);L). ↑P[x])) supposing 0 < last_index(L;x.P[x])

∧ ¬(∃x∈L. ↑P[x]) supposing last_index(L;x.P[x]) = 0 ∈ ℤ)

Proof

Definitions occuring in Statement : last_index: last_index(L;x.P[x]), l_exists: (∃x∈L. P[x]), select: L[n], nth_tl: nth_tl(n;as), list: T List, assert: ↑b, bool: 𝔹, less_than: a < b, uimplies: b supposing a, uall: ∀[x:A]. B[x], so_apply: x[s], not: ¬A, and: P ∧ Q, function: x:A ⟶ B[x], subtract: n - m, natural_number: $n, int: ℤ, universe: Type, equal: s = t ∈ T
Definitions unfolded in proof : uall: ∀[x:A]. B[x], member: t ∈ T, all: ∀x:A. B[x], nat: ℕ, implies: P ⇒ Q, false: False, ge: i ≥ j , uimplies: b supposing a, not: ¬A, satisfiable_int_formula: satisfiable_int_formula(fmla), exists: ∃x:A. B[x], top: Top, and: P ∧ Q, prop: ℙ, guard: {T}, or: P ∨ Q, cons: [a / b], le: A ≤ B, less_than': less_than'(a;b), so_apply: x[s], so_lambda: λ₂x.t[x], subtype_rel: A ⊆r B, decidable: Dec(P), less_than: a < b, squash: ↓T, int_seg: {i..j^-}, lelt: i ≤ j < k, colength: colength(L), nil: [], it: ⋅, sq_type: SQType(T), so_lambda: λ₂x y.t[x; y], so_apply: x[s1;s2], cand: A c∧ B, pi2: snd(t), select: L[n], last_index: last_index(L;x.P[x]), assert: ↑b, l_exists: (∃x∈L. P[x]), bool: 𝔹, unit: Unit, btrue: tt, uiff: uiff(P;Q), ifthenelse: if b then t else f fi , bfalse: ff, bnot: ¬_bb, rev_implies: P ⇐ Q, iff: P ⇐⇒ Q, subtract: n - m, nth_tl: nth_tl(n;as), le_int: i ≤z j, lt_int: i <z j, tl: tl(l), true: True
Lemmas referenced : nat_properties, full-omega-unsat, intformand_wf, intformle_wf, itermConstant_wf, itermVar_wf, intformless_wf, istype-int, int_formula_prop_and_lemma, istype-void, int_formula_prop_le_lemma, int_term_value_constant_lemma, int_term_value_var_lemma, int_formula_prop_less_lemma, int_formula_prop_wf, ge_wf, istype-less_than, assert_witness, intformeq_wf, int_formula_prop_eq_lemma, list-cases, product_subtype_list, colength-cons-not-zero, istype-nat, colength_wf_list, istype-false, istype-le, select_wf, subtract_wf, last_index_wf, decidable__le, intformnot_wf, itermSubtract_wf, int_formula_prop_not_lemma, int_term_value_subtract_lemma, non_neg_length, decidable__lt, length_wf, length_wf_nat, int_seg_properties, itermAdd_wf, int_term_value_add_lemma, subtract-1-ge-0, subtype_base_sq, set_subtype_base, int_subtype_base, spread_cons_lemma, decidable__equal_int, le_wf, list_wf, bool_wf, istype-universe, equal-wf-base, assert_wf, l_exists_wf_nil, less_than_wf, equal_wf, pi2_wf, ifthenelse_wf, nil_wf, list_accum_wf, nth_tl_nil, base_wf, stuck-spread, list_accum_nil_lemma, length_of_nil_lemma, last_index_cons, lt_int_wf, eqtt_to_assert, assert_of_lt_int, eqff_to_assert, bool_subtype_base, bool_cases_sqequal, assert-bnot, iff_weakening_uiff, select-cons-tl, add-associates, add-commutes, add-swap, zero-add, cons_wf, length_of_cons_lemma, length_cons, le_int_wf, assert_of_le_int, reduce_tl_cons_lemma, l_exists_cons, l_exists_wf, l_member_wf, istype-assert
Rules used in proof : sqequalSubstitution, sqequalTransitivity, computationStep, sqequalReflexivity, isect_memberFormation_alt, introduction, cut, thin, lambdaFormation_alt, extract_by_obid, sqequalHypSubstitution, isectElimination, hypothesisEquality, hypothesis, setElimination, rename, intWeakElimination, natural_numberEquality, independent_isectElimination, approximateComputation, independent_functionElimination, dependent_pairFormation_alt, lambdaEquality_alt, int_eqEquality, dependent_functionElimination, isect_memberEquality_alt, voidElimination, sqequalRule, independent_pairFormation, universeIsType, productElimination, independent_pairEquality, equalityTransitivity, equalitySymmetry, applyLambdaEquality, functionIsTypeImplies, inhabitedIsType, isectIsTypeImplies, unionElimination, promote_hyp, hypothesis_subsumption, equalityIsType1, dependent_set_memberEquality_alt, because_Cache, applyEquality, closedConclusion, imageElimination, addEquality, instantiate, equalityIsType4, baseApply, baseClosed, intEquality, functionIsType, universeEquality, isect_memberFormation, spreadEquality, lambdaEquality, productEquality, lambdaFormation, voidEquality, isect_memberEquality, dependent_pairFormation, cumulativity, equalityElimination, equalityIsType3, setIsType, unionIsType

Latex:
\mforall{}[T:Type]. \mforall{}[P:T {}\mrightarrow{} \mBbbB{}]. \mforall{}[L:T List]. ((\muparrow{}P[L[last\_index(L;x.P[x]) - 1]]) \mwedge{} (\mneg{}(\mexists{}x\mmember{}nth\_tl(last\_index(L;x.P[x]);L). \muparrow{}P[x])) supposing 0 < last\_index(L;x.P[x]) \mwedge{} \mneg{}(\mexists{}x\mmember{}L. \muparrow{}P[x]) supposing last\_index(L;x.P[x]) = 0) Date html generated: 2019_10_15-AM-11_10_27 Last ObjectModification: 2018_10_18-PM-11_52_11 Theory : general Home Index