This repository contains an example proof used as an exercise in comparing a variety of theorem provers.
The proof itself shows that a weakest precondition function for a simple imperative language agrees with a small-step operational semantics. It can be discharged by induction on the evaluation step taken, with minimal additional reasoning. However, this minimal reasoning takes different amounts of effort in different systems.