Nuprl - Proof: hsimp rec wd

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

'a:S.

all

(

x:'a. all

(

x:'a. (

f:'a

'a. all

(

x:'a. (

f:'a

'a. (

n:hnum. equal

(

x:'a. (

f:'a

'a. (

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

(

x:'a. (

f:'a

'a. (

n:hnum. ,simp_rec_fun(x,f,suc(n),n)))))

By:	HN THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Unab [`hsimp_rec`] THEN StrongAuto THEN Try (Complete (Unfold `label` 0)) THEN Simpsetp [`hol_to_nuprl`;`bequal`] THEN StrongAuto THEN Try (Complete (Unfold `label` 0))

Generated subgoal:

1 1. 'a : S
2. x : 'a
3. f : 'a 'a
4. n :
ncompose(f;n;x) = simp_rec_fun(x,f,n+1,n)
13 steps

About:

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