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