Even Length Append
------------------

Summary:
Needs induction scheme on two variable
Needs 1 lemmata

------

Definitions:

len
---

(len nil) = 0
(len (X::Y)) = (s (len Y))

even
----

(even 0) = true
(even (s 0)) = false
(even (s (s X))) = (even X)

app
---

(app nil Z) = Z
(app (X::Y) Z) = X::(app Y Z)


------

Theorem:

forall x:list(A), y:list(A).
	(even (len (app X Y))) = (even (len (app Y X)))

------

Comments:

Its the (non-mutually recursive) definition of even that requires a
non-straigtforward induction scheme.

A lemma is also required (along the lines of)

(len (app (X, Y1::Y2::Y))) = (s (s (len (app Y X))))

------

Source:

Andrew Ireland