Nuprl Lemma : lastn-nil

[n:ℤ]. (lastn(n;[]) [])


Proof




Definitions occuring in Statement :  lastn: lastn(n;L) nil: [] uall: [x:A]. B[x] int: sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B all: x:A. B[x] implies:  Q bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) and: P ∧ Q uimplies: supposing a ifthenelse: if then else fi  bfalse: ff guard: {T} prop: satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False not: ¬A top: Top
Lemmas referenced :  lastn-cases nil_wf top_wf length_of_nil_lemma reduce_tl_nil_lemma le_int_wf bool_wf equal-wf-base int_subtype_base assert_wf le_wf lt_int_wf less_than_wf bnot_wf uiff_transitivity eqtt_to_assert assert_of_le_int eqff_to_assert assert_functionality_wrt_uiff bnot_of_le_int assert_of_lt_int equal_wf satisfiable-full-omega-tt intformand_wf intformless_wf itermConstant_wf itermVar_wf int_formula_prop_and_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_var_lemma int_formula_prop_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesis hypothesisEquality sqequalAxiom intEquality natural_numberEquality baseApply closedConclusion baseClosed applyEquality because_Cache lambdaFormation unionElimination equalityElimination independent_functionElimination productElimination independent_isectElimination equalityTransitivity equalitySymmetry dependent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll

Latex:
\mforall{}[n:\mBbbZ{}].  (lastn(n;[])  \msim{}  [])



Date html generated: 2018_05_21-PM-06_31_06
Last ObjectModification: 2017_07_26-PM-04_51_07

Theory : general


Home Index