Wilmer Ricciotti's solution

- Authors: Wilmer Ricciotti
- Parts addressed: 1a
- Proof assistant / theorem prover used: Matita.
- Encoding technique: Locally nameless.
- Files: available from the author's page.

Wilmer Ricciotti's solution

- Authors: Wilmer Ricciotti
- Parts addressed: 1a
- Proof assistant / theorem prover used: Matita.
- Encoding technique: Locally nameless.
- Files: available from the author's page.

Commentary

- This solution was meant as a test case for the Matita, an interactive theorem prover currently under development at the University of Bologna.
- A first version of the solution followed closely Leroy's swap-based approach.
- The current version of the solution follows closely the specifications, through the use of a hybrid inversion/induction principle.
- A formalization of the proof of adequacy for the locally nameless encoding is also provided.