Nuprl - hol_prim_rec LEMMAs for prim_rec

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

Theorem	Name
Thm* 'a:S, x:'a, f:('a'a). Thm* (n:. prim_rec_fun(x,f,0,n) = x) Thm* & (m,n:. prim_rec_fun(x,f,m+1,n) = f(prim_rec_fun(x,f,m,pre(n)),n))	[prim_rec_eqn]
cites the following:
Thm* 'a:S. Thm* all Thm* (x:'a. all Thm* (x:'a. (f:'a hnum 'a. and Thm* (x:'a. (f:'a hnum 'a. (all(n:hnum. equal(prim_rec_fun(x,f,0,n),x)) Thm* (x:'a. (f:'a hnum 'a. ,all Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. all Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. equal Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. (prim_rec_fun Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ((x Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. (,f Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. (,suc(m) Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. (,n) Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,f Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,(prim_rec_fun Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,((x Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,(,f Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,(,m Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,(,pre(n)) Thm* (x:'a. (f:'a hnum 'a. ,(m:hnum. (n:hnum. ,,n)))))))	[hprim_rec_eqn]

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