Nuprl - hol_arithmetic_4 LEMMAs for mult

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

Theorem	Name
Thm* m,n:. Thm* 0m = 0 Thm* & m0 = 0 Thm* & 1m = m Thm* & m1 = m Thm* & (m+1)n = mn+n Thm* & m(n+1) = m+mn	[mult_clauses]
cites the following:
Thm* all Thm* (m:hnum. all Thm* (m:hnum. (n:hnum. and Thm* (m:hnum. (n:hnum. (equal(mult(0,m),0) Thm* (m:hnum. (n:hnum. ,and Thm* (m:hnum. (n:hnum. ,(equal(mult(m,0),0) Thm* (m:hnum. (n:hnum. ,,and Thm* (m:hnum. (n:hnum. ,,(equal(mult(1,m),m) Thm* (m:hnum. (n:hnum. ,,,and Thm* (m:hnum. (n:hnum. ,,,(equal(mult(m,1),m) Thm* (m:hnum. (n:hnum. ,,,,and Thm* (m:hnum. (n:hnum. ,,,,(equal(mult(suc(m),n),add(mult(m,n),n)) Thm* (m:hnum. (n:hnum. ,,,,,equal(mult(m,suc(n)),add(m,mult(m,n))))))))))	[hmult_clauses]

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