m,n,x:
. m+(n+x) = (m+n)+x 
Thm* (
m:hnum. all
Thm* (
m:hnum. (n:hnum. all(p:hnum. equal(add(m,add(n,p)),add(add(m,n),p)))))| Theorem | Name |
| m,n,x:. m+(n+x) = (m+n)+x | [add_assoc] |
| cites the following: | |
Thm* ( m:hnum. all
Thm* ( m:hnum. (n:hnum. all(p:hnum. equal(add(m,add(n,p)),add(add(m,n),p))))) | [hadd_assoc] |