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.

翻译：重写归纳（RI）是一种用于证明项上的方程是重写系统的归纳定理的原理，即该方程的任意基实例都是该重写系统的定理。RI已适用于多种类型的重写系统，并且针对约束重写系统的RI已扩展到不等式。在本文中，我们将针对约束方程的RI扩展到逻辑约束重写中存在量化的方程。为此，我们首先通过向约束方程的方程部分引入存在量化来扩展约束方程。然后，在将约束重写规则应用于此类扩展的约束方程时，我们向所应用规则的额外变量引入存在量化。最后，利用约束重写规则的扩展应用，我们将针对约束方程的RI扩展到存在量化方程。