Nuprl Lemma : primrec-unroll
∀[n:ℤ]. ∀[b,c:Top]. (primrec(n;b;c) ~ if n <z 1 then b else c (n - 1) primrec(n - 1;b;c) fi )
Proof
Definitions occuring in Statement :
primrec: primrec(n;b;c),
ifthenelse: if b then t else f fi ,
lt_int: i <z j,
uall: ∀[x:A]. B[x],
top: Top,
apply: f a,
subtract: n - m,
natural_number: $n,
int: ℤ,
sqequal: s ~ t
Definitions unfolded in proof :
primrec: primrec(n;b;c)
Lemmas referenced :
primtailrec-unroll
Rules used in proof :
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
hypothesis
Latex:
\mforall{}[n:\mBbbZ{}]. \mforall{}[b,c:Top]. (primrec(n;b;c) \msim{} if n <z 1 then b else c (n - 1) primrec(n - 1;b;c) fi )
Date html generated:
2019_06_20-AM-11_27_30
Last ObjectModification:
2019_01_28-PM-05_04_44
Theory : call!by!value_2
Home
Index