Implicit induction techniques for the verification of PIM : a transformational toolkit for compilers

The development of the proof techniques presented in this paper was inspired by a proof problem for Pim -- a transformational toolkit for compilers. Pim consists of the untyped lambda calculus extended with an algebraic rewriting system that characterizes the behavior of lazy stores and generalized conditionals. The first-order algebraic component of Pim has an omega-complete conservative extension. Showing conservativeness of the extension requires proving that the additional equations of the extension are inductive consequences of the initial axioms. The complexity of the manual proofs motivated us to look into the current implicit induction procedures w.r.t. their applicability to this proof problem. However, the existing implicit induction methods turned out to be inadequate. In this paper we propose new implicit induction techniques adequate for solving the indicated proof problem.