Nuprl - Proof: prim rec eqn

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

'a:S, x:'a, f:('a

'a).

(

. prim_rec_fun(x,f,0,n) = x)

& (

m,n:

. prim_rec_fun(x,f,m+1,n) = f(prim_rec_fun(x,f,m,pre(n)),n))

By:	RewriteOfThm Thm: hprim rec eqn (SimpsetC [`hol_to_nuprl`;`bequal`]) THEN Try (Complete (Unfold `hnum` 0))

Generated subgoals:

None

About:

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