Matthew Fairbairn's solution

• Author: Matthew Fairbairn.
• Parts addressed: 3.
• Proof assistant / theorem prover used: Alpha Prolog.
• Encoding technique: Nominal Representation.
• Files: [tar.gz]

Commentary

This submission was constructed as an example to clarify what was meant by the term "animation" in the challenge.