Nuprl - Proof: hadd clauses

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: hadd clauses

all

(

n:hnum. all

(

n:hnum. (

m:hnum. and

(

n:hnum. (

m:hnum. (equal(add(0,m),m)

(

n:hnum. (

m:hnum. ,and

(

n:hnum. (

m:hnum. ,(equal(add(m,0),m)

(

n:hnum. (

m:hnum. ,,and

(

n:hnum. (

m:hnum. ,,(equal(add(suc(m),n),suc(add(m,n)))

(

n:hnum. (

m:hnum. ,,,equal(add(m,suc(n)),suc(add(m,n))))))))

By:	HOL "hadd_clauses"

Generated subgoals:

None

About:

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