Nuprl Lemma : fast-fib-ext

n:ℕ(∃m:{ℕ(m fib(n) ∈ ℕ)})


Proof




Definitions occuring in Statement :  fib: fib(n) nat: all: x:A. B[x] sq_exists: x:{A| B[x]} equal: t ∈ T
Definitions unfolded in proof :  member: t ∈ T fast-fib natrec: natrec genrec: genrec so_apply: x[s1;s2] decidable__equal_int decidable__int_equal uall: [x:A]. B[x] so_lambda: so_lambda(x,y,z,w.t[x; y; z; w]) so_apply: x[s1;s2;s3;s4] so_lambda: λ2x.t[x] top: Top so_apply: x[s] uimplies: supposing a strict4: strict4(F) and: P ∧ Q all: x:A. B[x] implies:  Q has-value: (a)↓ prop: guard: {T} or: P ∨ Q squash: T subtract: m genrec-ap: genrec-ap
Lemmas referenced :  fast-fib lifting-strict-int_eq top_wf equal_wf has-value_wf_base base_wf is-exception_wf decidable__equal_int decidable__int_equal
Rules used in proof :  introduction sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity cut instantiate extract_by_obid hypothesis sqequalRule thin sqequalHypSubstitution isectElimination baseClosed isect_memberEquality voidElimination voidEquality independent_isectElimination independent_pairFormation lambdaFormation callbyvalueDecide hypothesisEquality equalityTransitivity equalitySymmetry unionEquality unionElimination sqleReflexivity dependent_functionElimination independent_functionElimination baseApply closedConclusion decideExceptionCases inrFormation because_Cache imageMemberEquality imageElimination exceptionSqequal inlFormation

Latex:
\mforall{}n:\mBbbN{}.  (\mexists{}m:\{\mBbbN{}|  (m  =  fib(n))\})



Date html generated: 2017_04_17-AM-09_44_18
Last ObjectModification: 2017_02_27-PM-05_38_28

Theory : num_thy_1


Home Index