Nuprl Lemma : primrec1_lemma
∀c,b:Top. (primrec(1;b;c) ~ c 0 b)
Proof
Definitions occuring in Statement :
primrec: primrec(n;b;c),
top: Top,
all: ∀x:A. B[x],
apply: f a,
natural_number: $n,
sqequal: s ~ t
Definitions unfolded in proof :
all: ∀x:A. B[x],
primrec: primrec(n;b;c),
primtailrec: primtailrec(n;i;b;f),
subtract: n - m,
member: t ∈ T
Lemmas referenced :
istype-top
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
Error :lambdaFormation_alt,
cut,
sqequalRule,
hypothesis,
Error :inhabitedIsType,
hypothesisEquality,
introduction,
extract_by_obid
Latex:
\mforall{}c,b:Top. (primrec(1;b;c) \msim{} c 0 b)
Date html generated:
2019_06_20-AM-11_27_43
Last ObjectModification:
2019_01_28-PM-05_30_36
Theory : call!by!value_2
Home
Index