Nuprl - Proof: hprim rec thm

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hprim rec thm

'a:S.

all

(

x:'a. all

(

x:'a. (

f:'a

hnum

'a. and

(

x:'a. (

f:'a

hnum

'a. (equal(prim_rec(x,f,0),x)

(

x:'a. (

f:'a

hnum

'a. ,all

(

x:'a. (

f:'a

hnum

'a. ,(

m:hnum. equal

(

x:'a. (

f:'a

hnum

'a. ,(

m:hnum. (prim_rec(x,f,suc(m))

(

x:'a. (

f:'a

hnum

'a. ,(

m:hnum. ,f(prim_rec(x,f,m),m))))))

By:	HOL "hprim_rec_thm"

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html