### Nuprl Lemma : last-lemma-sq

`∀[T:Type]. ∀[L:T List].  L ~ firstn(||L|| - 1;L) @ [last(L)] supposing ¬↑null(L)`

Proof

Definitions occuring in Statement :  firstn: `firstn(n;as)` last: `last(L)` length: `||as||` null: `null(as)` append: `as @ bs` cons: `[a / b]` nil: `[]` list: `T List` assert: `↑b` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` not: `¬A` subtract: `n - m` natural_number: `\$n` universe: `Type` sqequal: `s ~ t`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` prop: `ℙ` not: `¬A` implies: `P `` Q` uiff: `uiff(P;Q)` and: `P ∧ Q` gt: `i > j` all: `∀x:A. B[x]` or: `P ∨ Q` false: `False` cons: `[a / b]` top: `Top` guard: `{T}` nat: `ℕ` le: `A ≤ B` decidable: `Dec(P)` iff: `P `⇐⇒` Q` rev_implies: `P `` Q` subtract: `n - m` subtype_rel: `A ⊆r B` less_than': `less_than'(a;b)` true: `True` squash: `↓T` int_iseg: `{i...j}` cand: `A c∧ B` less_than: `a < b` satisfiable_int_formula: `satisfiable_int_formula(fmla)` exists: `∃x:A. B[x]` last: `last(L)` ge: `i ≥ j ` int_seg: `{i..j-}` lelt: `i ≤ j < k`
Lemmas referenced :  not_wf assert_wf null_wf list_wf assert_of_null equal-wf-T-base list-cases length_of_nil_lemma nil_wf product_subtype_list length_of_cons_lemma length_wf_nat nat_wf decidable__lt false_wf not-lt-2 condition-implies-le minus-add minus-one-mul zero-add minus-one-mul-top add-commutes add_functionality_wrt_le add-associates add-zero le-add-cancel equal_wf list_decomp nth_tl_wf subtract_wf length_wf less_than_wf squash_wf true_wf length_nth_tl decidable__le satisfiable-full-omega-tt intformand_wf intformnot_wf intformle_wf itermConstant_wf itermSubtract_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_subtract_lemma int_term_value_var_lemma int_formula_prop_less_lemma int_formula_prop_wf le_wf iff_weakening_equal select-nthtl subtype_rel_list top_wf decidable__equal_int intformeq_wf int_formula_prop_eq_lemma reduce_tl_nil_lemma reduce_tl_cons_lemma equal-wf-base non_neg_length nat_properties itermAdd_wf int_term_value_add_lemma append_firstn_lastn_sq lelt_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut hypothesis sqequalAxiom extract_by_obid sqequalHypSubstitution isectElimination thin cumulativity hypothesisEquality sqequalRule isect_memberEquality because_Cache equalityTransitivity equalitySymmetry universeEquality lambdaFormation independent_functionElimination productElimination independent_isectElimination baseClosed promote_hyp dependent_functionElimination unionElimination voidElimination hypothesis_subsumption voidEquality setElimination rename natural_numberEquality addEquality independent_pairFormation applyEquality lambdaEquality intEquality minusEquality imageElimination dependent_set_memberEquality dependent_pairFormation int_eqEquality computeAll productEquality imageMemberEquality applyLambdaEquality

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].    L  \msim{}  firstn(||L||  -  1;L)  @  [last(L)]  supposing  \mneg{}\muparrow{}null(L)

Date html generated: 2017_04_17-AM-07_33_17
Last ObjectModification: 2017_02_27-PM-04_11_03

Theory : list_1

Home Index