Two Definitions of Even are Equivalent
--------------------------------------

------
Summary:
Mutual Recursion

------
Defintions:

evenm
-----

nat -> bool

(evenm 0) = true
(evenm (s N)) = (oddm N)

oddm
----

nat -> bool

(oddm 0) = false
(oddm (s N)) = (evenm N)

evenr
-----

nat -> bool

(evenr 0) = true
(evenr (s 0)) = false
(evenr (s (s N))) = (evenr N)

Theorem
-------

forall n:nat
	(evenm n) = (evenr n)

Source
------

Alan Bundy