n:
. (even(n) 
(
m:. n = 2
m 
)) & (odd(n) (m:. n = 2m+1 ))Thm* (
n:hnum. and
Thm* (
n:hnum. (implies(even(n),exists(m:hnum. equal(n,mult(2,m))))
Thm* (
n:hnum. ,implies(odd(n),exists(m:hnum. equal(n,suc(mult(2,m)))))))| Theorem | Name |
| n:. (even(n) (m:. n = 2m )) & (odd(n) (m:. n = 2m+1 )) | [even_odd_exists] |
| cites the following: | |
Thm* ( n:hnum. and
Thm* ( n:hnum. (implies(even(n),exists(m:hnum. equal(n,mult(2,m))))
Thm* ( n:hnum. ,implies(odd(n),exists(m:hnum. equal(n,suc(mult(2,m))))))) | [heven_odd_exists] |