Nuprl Lemma : select_cons_tl_sq2

[i:ℕ]. ∀[x,l:Top].  ([x l][i 1] l[i])


Proof




Definitions occuring in Statement :  select: L[n] cons: [a b] nat: uall: [x:A]. B[x] top: Top add: m natural_number: $n sqequal: t
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T nat: uimplies: supposing a ge: i ≥  all: x:A. B[x] decidable: Dec(P) or: P ∨ Q not: ¬A implies:  Q satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] false: False top: Top and: P ∧ Q prop:
Lemmas referenced :  select-cons-tl nat_properties decidable__lt full-omega-unsat intformand_wf intformnot_wf intformless_wf itermConstant_wf itermAdd_wf itermVar_wf intformle_wf int_formula_prop_and_lemma int_formula_prop_not_lemma int_formula_prop_less_lemma int_term_value_constant_lemma int_term_value_add_lemma int_term_value_var_lemma int_formula_prop_le_lemma int_formula_prop_wf add-subtract-cancel top_wf nat_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalRule extract_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality addEquality setElimination rename hypothesis natural_numberEquality independent_isectElimination dependent_functionElimination unionElimination approximateComputation independent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality isect_memberEquality voidElimination voidEquality independent_pairFormation sqequalAxiom because_Cache

Latex:
\mforall{}[i:\mBbbN{}].  \mforall{}[x,l:Top].    ([x  /  l][i  +  1]  \msim{}  l[i])



Date html generated: 2018_05_21-PM-06_20_16
Last ObjectModification: 2018_05_19-PM-05_32_24

Theory : list!


Home Index