n:. (even(n)  (m:. n = 2m  )) & (odd(n)  (m:. n = 2m+1  ))

By:	RewriteOfThm Thm* all Thm* (n:hnum. and Thm* (n:hnum. (implies(even(n),exists(m:hnum. equal(n,mult(2,m)))) Thm* (n:hnum. ,implies(odd(n),exists(m:hnum. equal(n,suc(mult(2,m))))))) (SimpsetC [`hol_to_nuprl`;`bequal`])

None

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