Nuprl - Proof: hmult clauses

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

all

(

m:hnum. all

(

m:hnum. (

n:hnum. and

(

m:hnum. (

n:hnum. (equal(mult(0,m),0)

(

m:hnum. (

n:hnum. ,and

(

m:hnum. (

n:hnum. ,(equal(mult(m,0),0)

(

m:hnum. (

n:hnum. ,,and

(

m:hnum. (

n:hnum. ,,(equal(mult(1,m),m)

(

m:hnum. (

n:hnum. ,,,and

(

m:hnum. (

n:hnum. ,,,(equal(mult(m,1),m)

(

m:hnum. (

n:hnum. ,,,,and

(

m:hnum. (

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

(

m:hnum. (

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

By:	HOL "hmult_clauses"

Generated subgoals:

None

About:

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