Nuprl Lemma : nth_tl_decomp_eq

[T:Type]. ∀[m:ℕ]. ∀[L:T List].  nth_tl(m;L) [L[m] nth_tl(1 m;L)] ∈ (T List) supposing m < ||L||


Proof




Definitions occuring in Statement :  select: L[n] length: ||as|| nth_tl: nth_tl(n;as) cons: [a b] list: List nat: less_than: a < b uimplies: supposing a uall: [x:A]. B[x] add: m natural_number: $n universe: Type equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T uimplies: supposing a nat: ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False implies:  Q not: ¬A top: Top and: P ∧ Q prop:
Lemmas referenced :  nat_wf list_wf length_wf less_than_wf nth_tl_wf int_formula_prop_wf int_term_value_var_lemma int_term_value_constant_lemma int_formula_prop_le_lemma int_formula_prop_not_lemma int_formula_prop_and_lemma itermVar_wf itermConstant_wf intformle_wf intformnot_wf intformand_wf satisfiable-full-omega-tt decidable__le nat_properties select_wf cons_wf nth_tl_decomp
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality independent_isectElimination hypothesis cumulativity because_Cache setElimination rename dependent_functionElimination natural_numberEquality unionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation computeAll addEquality axiomEquality equalityTransitivity equalitySymmetry universeEquality

Latex:
\mforall{}[T:Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[L:T  List].    nth\_tl(m;L)  =  [L[m]  /  nth\_tl(1  +  m;L)]  supposing  m  <  ||L||



Date html generated: 2016_05_14-AM-07_37_23
Last ObjectModification: 2016_01_15-AM-08_43_35

Theory : list_1


Home Index