Nuprl - Proof: hprim rec fun wd

PrintForm Definitions hol prim rec Sections HOLlib Doc

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

'a:S.

all

(

x:'a. all

(

x:'a. (

f:'a

hnum

'a. equal

(

x:'a. (

f:'a

hnum

'a. (prim_rec_fun(x,f)

(

x:'a. (

f:'a

hnum

'a. ,simp_rec

(

x:'a. (

f:'a

hnum

'a. ,((

n:hnum. x)

(

x:'a. (

f:'a

hnum

'a. ,,

fun:hnum

'a.

n:hnum. f

(

x:'a. (

f:'a

hnum

'a. ,,

fun:hnum

'a.

n:hnum. (fun(pre(n))

(

x:'a. (

f:'a

hnum

'a. ,,

fun:hnum

'a.

n:hnum. ,n)))))

By:	Unab [`hprim_rec_fun`] THEN HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoals:

None

About:

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

PrintForm Definitions hol prim rec Sections HOLlib Doc