Nuprl Lemma : ctrex1-calculation
small-ctrex1() 10^1143 ~ 23
Proof
Definitions occuring in Statement :
small-ctrex1: small-ctrex1(),
apply: f a,
natural_number: $n,
sqequal: s ~ t,
fastexp: i^n
Definitions unfolded in proof :
prop: ℙ,
implies: P ⇒ Q,
not: ¬A,
false: False,
less_than': less_than'(a;b),
and: P ∧ Q,
le: A ≤ B,
nat: ℕ,
uimplies: b supposing a,
member: t ∈ T,
uall: ∀[x:A]. B[x],
has-value: (a)↓,
small-ctrex1: small-ctrex1()
Lemmas referenced :
value-type-has-value,
int-value-type,
fastexp_wf,
false_wf,
le_wf
Rules used in proof :
sqequalSubstitution,
because_Cache,
hypothesisEquality,
lambdaFormation,
independent_pairFormation,
dependent_set_memberEquality,
natural_numberEquality,
hypothesis,
independent_isectElimination,
intEquality,
thin,
isectElimination,
sqequalHypSubstitution,
lemma_by_obid,
cut,
computationStep,
sqequalTransitivity,
callbyvalueReduce,
sqequalReflexivity,
sqequalRule,
computeAll
Latex:
small-ctrex1() 10\^{}1143 \msim{} 23
Date html generated:
2016_05_18-AM-10_48_30
Last ObjectModification:
2016_01_07-PM-09_23_44
Theory : reals
Home
Index