Rotate Length
-------------

Summary:
Lemmas Required

------
Definitions:

len
---

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

app
---

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

rotate
------

(rotate 0 Z) = Z
(rotate (s X) nil) = nil
(rotate (s X) (Y::Z)) = (rotate X (app Z (Y::nil)))

------

Theorem:

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

------

Comments:

Needs lemmata

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

------
Source:

Andrew Ireland