Nuprl - Proof: hsimp rec thm

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

'a:S.

all

(

x:'a. all

(

x:'a. (

f:'a

'a. and

(

x:'a. (

f:'a

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

(

x:'a. (

f:'a

'a. ,all

(

x:'a. (

f:'a

'a. ,(

m:hnum. equal

(

x:'a. (

f:'a

'a. ,(

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

(

x:'a. (

f:'a

'a. ,(

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

By:	HOL "hsimp_rec_thm"

Generated subgoals:

None

About:

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