Nuprl Lemma : primrec1_lemma

c,b:Top.  (primrec(1;b;c) b)


Proof




Definitions occuring in Statement :  primrec: primrec(n;b;c) top: Top all: x:A. B[x] apply: a natural_number: $n sqequal: t
Definitions unfolded in proof :  all: x:A. B[x] primrec: primrec(n;b;c) primtailrec: primtailrec(n;i;b;f) subtract: 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