n:
. 
m:. n = (0+1+1)
m 
n = (0+1+1)m+1 Thm* (
n:hnum. exists
Thm* (
n:hnum. (m:hnum. or
Thm* (
n:hnum. (m:hnum. (equal(n,mult(suc(suc(0)),m))
Thm* (
n:hnum. (m:hnum. ,equal(n,add(mult(suc(suc(0)),m),1)))))| Theorem | Name |
| n:. m:. n = (0+1+1)m n = (0+1+1)m+1 | [odd_or_even] |
| cites the following: | |
Thm* ( n:hnum. exists
Thm* ( n:hnum. (m:hnum. or
Thm* ( n:hnum. (m:hnum. (equal(n,mult(suc(suc(0)),m))
Thm* ( n:hnum. (m:hnum. ,equal(n,add(mult(suc(suc(0)),m),1))))) | [hodd_or_even] |