Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version)

TL;DR

This paper extends Rewriting Induction (RI) to handle existentially quantified equations within logically constrained rewriting, enabling more expressive proofs of inductive theorems involving existential quantifiers.

Contribution

The paper introduces a novel extension of RI that incorporates existential quantification into constrained equations and rewrite rules, broadening its applicability.

Findings

Extended RI to existentially quantified equations.

Introduced existential quantification in rule application.

Enhanced proof capabilities for logical constraints.

Abstract

Rewriting Induction (RI) is a principle to prove that an equation over terms is an inductive theorem of a rewrite system, i.e., that any ground instance of the equation is a theorem of the rewrite system. RI has been adapted to several kinds of rewrite systems, and RI for constrained rewrite systems has been extended to inequalities. In this paper, we extend RI for constrained equations to existentially quantified equations in logically constrained rewriting. To this end, we first extend constrained equations by introducing existential quantification to the equation part of constrained equations. Then, in applying a constrained rewrite rule to such extended constrained equations, we introduce existential quantification to extra variables of the applied rule. Finally, using the extended application of constrained rewrite rules, we extend RI for constrained equations to existentially quantified equations.