The Z-property for left-linear term rewriting via convective context-sensitive completeness


We present a method to derive the Z-property, hence confluence, of a first-order term rewrite system T from completeness of an associated context-sensitive term rewrite system T,μ with replacement map μ. We generalise earlier such results by only requiring left-linearity of T and that T-critical peaks be T,μ-critical peaks. We introduce convective replacement maps as a generalisation of the canonical maps known from the literature.