Left-linear Bounded TRSs are Inverse Recognizability Preserving

IrèNe Durand & Marc Sylvestre
Bounded rewriting for linear term rewriting systems has been defined in (I. Durand, G. Sénizergues, M. Sylvestre. Termination of linear bounded term rewriting systems. Proceedings of the 21st International Conference on Rewriting Techniques and Applications) as a restriction of the usual notion of rewriting. We extend here this notion to the whole class of left-linear term rewriting systems, and we show that bounded rewriting is effectively inverse-recognizability preserving. The bounded class (BO) is, by definition,...