# The Mechanisation of Barendregt-Style Equational Proofs

## (The Residual Perspective)

### Authors: Rene Vestergaard and James Brotherston

The Isabelle theories below comprise the Isabelle
/ HOL implementation of the proof of the results in section 3 of the
the article. All proofs are due to the authors. Queries
or comments are naturally welcome and may be directed either to Rene Vestergaard or James Brotherston.

View theory dependencies

## Theories

- Variables - Definition and properties
of the set of one-sorted variable names - in particular, the
guaranteed existence of fresh names
- MarkedLambda - Definition of
(marked) terms and substitution in the raw calculus, plus renaming and
substitution lemmas
- ResidualBeta - Proof of non-blocked
BCF-initial beta-residual theory , plus auxiliary lemmas