Confluent term rewriting systems with membership conditions

We propose a new type of conditional term rewriting system: the membership-conditional term rewriting system, in which, each rewriting rule can have membership conditions which restrict the substitution values for the variables occurring in the rule. For example, the rule f(x, x, y) ▹ g(x, y) if x ∈ T' yields the reduction f(M, M, N) → g(M, N) only when M is in the term set T'. Thus, by using membership-conditional rewriting, we can easily provide a strategy for term reduction. We study the confluence of membership-conditional term rewriting systems that are nonterminating and nonlinear. It is shown that a restricted nonlinear term rewriting system in which membership conditions satisfy the closure and termination properties is confluent if the system is nonoverlapping.