Nuprl - Proof: odd or even

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: odd or even

. n = (0+1+1)

n = (0+1+1)

m+1

By:	RewriteOfThm Thm* all Thm* (n:hnum. exists Thm* (n:hnum. (m:hnum. or Thm* (n:hnum. (m:hnum. (equal(n,mult(suc(suc(0)),m)) Thm* (n:hnum. (m:hnum. ,equal(n,add(mult(suc(suc(0)),m),1))))) (SimpsetC [`hol_to_nuprl`;`bequal`])

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html