Infinite normal forms for non linear term rewriting systems

In this paper we discuss the applicability of the framework defined in [DK89, DKP89, DKP90] on the existence of infinite normal forms on a particular class of non left linear term rewriting system. It is very common, in practice, to deal with non linear term rewriting systems especially when one wants to axiomatize the semantics of a given structure, and the purpose of this paper is that of showing that under some hypotheses it is possible to extend the results of [DK89, DKP89, DKP90] to a class of non left linear term rewriting system. Although, at a first glance the class we consider can appear quite restrictive, in practice it captures a number of algebric structures largely used in computer science.