Termination of Innermost-Terminating Right-Linear Overlay Term Rewrite Systems (Full Version)
This is an incremental theoretical result for the term rewriting community, providing a specific condition under which termination analysis can be simplified.
The paper tackled the problem of proving termination for right-linear overlay term rewrite systems by showing that termination is equivalent to innermost termination, meaning any rewrite sequence to a normal form can be simulated by innermost reduction.
It has been shown that, regarding a terminating right-linear overlay term rewrite system (TRS), any rewrite sequence ending with a normal form can be simulated by the innermost reduction. In this paper, using this simulation property, we show that for a right-linear overlay TRS, there is no infinite minimal dependency-pair chain if and only if there is no infinite innermost minimal dependency-pair chain. This implies that a right-linear overlay TRS is terminating if and only if it is innermost terminating.