n:
. even(n) 
(
m:. n = 2
m 
)
n:hnum. equal(even(n),exists(m:hnum. equal(n,mult(2,m)))))| Theorem | Name |
| n:. even(n) (m:. n = 2m ) | [even_exists] |
| cites the following: | |
| n:hnum. equal(even(n),exists(m:hnum. equal(n,mult(2,m))))) | [heven_exists] |