Nuprl Lemma : primrec0_lemma
∀c,b:Top. (primrec(0;b;c) ~ b)
Proof
Definitions occuring in Statement :
primrec: primrec(n;b;c),
top: Top,
all: ∀x:A. B[x],
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),
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(0;b;c) \msim{} b)
Date html generated:
2019_06_20-AM-11_27_42
Last ObjectModification:
2019_01_28-PM-05_28_56
Theory : call!by!value_2
Home
Index