Nuprl - hol_arithmetic_3 LEMMAs for add

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

Theorem	Name
Thm* n,m:. Thm* 0+m = m & m+0 = m & m+1+n = m+n+1 & m+(n+1) = (m+n)+1	[add_clauses]
cites the following:
Thm* all Thm* (n:hnum. all Thm* (n:hnum. (m:hnum. and Thm* (n:hnum. (m:hnum. (equal(add(0,m),m) Thm* (n:hnum. (m:hnum. ,and Thm* (n:hnum. (m:hnum. ,(equal(add(m,0),m) Thm* (n:hnum. (m:hnum. ,,and Thm* (n:hnum. (m:hnum. ,,(equal(add(suc(m),n),suc(add(m,n))) Thm* (n:hnum. (m:hnum. ,,,equal(add(m,suc(n)),suc(add(m,n))))))))	[hadd_clauses]

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