Nuprl Lemma : less-efficient-exp-ext

i:ℤ. ∀n:ℕ.  (∃j:{ℤ(j i^n ∈ ℤ)})


Proof




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

Latex:
\mforall{}i:\mBbbZ{}.  \mforall{}n:\mBbbN{}.    (\mexists{}j:\{\mBbbZ{}|  (j  =  i\^{}n)\})



Date html generated: 2016_07_08-PM-05_05_04
Last ObjectModification: 2016_07_05-PM-02_44_11

Theory : general


Home Index