Nuprl Lemma : nth-fibs

n:ℕ(s-nth(n;fibs()) fib(n) ∈ ℤ)


Proof




Definitions occuring in Statement :  fibs: fibs() fib: fib(n) s-nth: s-nth(n;s) nat: all: x:A. B[x] int: equal: t ∈ T
Definitions unfolded in proof :  all: x:A. B[x] uall: [x:A]. B[x] member: t ∈ T nat: implies:  Q false: False ge: i ≥  uimplies: supposing a not: ¬A satisfiable_int_formula: satisfiable_int_formula(fmla) exists: x:A. B[x] top: Top and: P ∧ Q prop: guard: {T} int_seg: {i..j-} lelt: i ≤ j < k decidable: Dec(P) or: P ∨ Q subtype_rel: A ⊆B so_lambda: λ2x.t[x] so_apply: x[s] sq_type: SQType(T) fibs: fibs() fib: fib(n) s-nth: s-nth(n;s) s-cons: x.s bool: 𝔹 unit: Unit it: btrue: tt uiff: uiff(P;Q) ifthenelse: if then else fi  bfalse: ff bnot: ¬bb assert: b bor: p ∨bq le: A ≤ B less_than': less_than'(a;b) int_upper: {i...} has-value: (a)↓ nequal: a ≠ b ∈  squash: T true: True iff: ⇐⇒ Q rev_implies:  Q subtract: m
Lemmas referenced :  nat_properties full-omega-unsat intformand_wf intformle_wf itermConstant_wf itermVar_wf intformless_wf int_formula_prop_and_lemma 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 less_than_wf int_seg_wf int_seg_properties decidable__le subtract_wf intformnot_wf itermSubtract_wf int_formula_prop_not_lemma int_term_value_subtract_lemma decidable__equal_int subtype_base_sq set_subtype_base int_subtype_base intformeq_wf int_formula_prop_eq_lemma decidable__lt lelt_wf subtype_rel_self le_wf eq_int_wf bool_wf eqtt_to_assert assert_of_eq_int testxxx_lemma eqff_to_assert equal_wf bool_cases_sqequal bool_subtype_base assert-bnot neg_assert_of_eq_int upper_subtype_nat false_wf nequal-le-implies zero-add value-type-has-value int-value-type int_upper_properties itermAdd_wf int_term_value_add_lemma nat_wf nth-stream-zip fibs_wf stream-subtype top_wf s-tl_wf add-commutes fib_wf squash_wf true_wf iff_weakening_equal add-associates add-swap not-le-2 not-equal-2 condition-implies-le minus-one-mul minus-one-mul-top minus-add minus-minus add_functionality_wrt_le le-add-cancel minus-zero add-zero le-add-cancel-alt s-nth_wf s_tl_cons_lemma s-cons_wf stream-zip_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut thin introduction extract_by_obid sqequalHypSubstitution isectElimination hypothesisEquality hypothesis setElimination rename intWeakElimination natural_numberEquality independent_isectElimination approximateComputation independent_functionElimination dependent_pairFormation lambdaEquality int_eqEquality intEquality dependent_functionElimination isect_memberEquality voidElimination voidEquality sqequalRule independent_pairFormation axiomEquality because_Cache productElimination unionElimination applyEquality instantiate equalityTransitivity equalitySymmetry applyLambdaEquality dependent_set_memberEquality hypothesis_subsumption equalityElimination promote_hyp cumulativity callbyvalueReduce addEquality imageElimination universeEquality imageMemberEquality baseClosed minusEquality

Latex:
\mforall{}n:\mBbbN{}.  (s-nth(n;fibs())  =  fib(n))



Date html generated: 2018_05_21-PM-00_59_57
Last ObjectModification: 2018_05_19-AM-06_36_41

Theory : num_thy_1


Home Index