x,q,n:
. exp(n;x+q) = exp(n;x)
exp(n;q)Thm* (
p:hnum. all
Thm* (
p:hnum. (q:hnum. all
Thm* (
p:hnum. (q:hnum. (n:hnum. equal
Thm* (
p:hnum. (q:hnum. (n:hnum. (exp(n,add(p,q))
Thm* (
p:hnum. (q:hnum. (n:hnum. ,mult(exp(n,p),exp(n,q))))))| Theorem | Name |
| x,q,n:. exp(n;x+q) = exp(n;x)exp(n;q) | [exp_add] |
| cites the following: | |
Thm* ( p:hnum. all
Thm* ( p:hnum. (q:hnum. all
Thm* ( p:hnum. (q:hnum. (n:hnum. equal
Thm* ( p:hnum. (q:hnum. (n:hnum. (exp(n,add(p,q))
Thm* ( p:hnum. (q:hnum. (n:hnum. ,mult(exp(n,p),exp(n,q)))))) | [hexp_add] |