The Z-property and ω-confluence by context-sensitive termination


We present a method to derive the Z-property for a first-order term rewrite system T from completeness of an associated context-sensitive term rewrite system T,μ with replacement map μ. By only requiring left-linearity of T and that T-critical peaks are also T,μ-critical peaks, we generalise results in the literature. In particular we allow completeness of T,μ to be established in arbitrary ways, not necessarily by means level-decreasingness or variations thereof as usually assumed. We answer the first of two open problems raised by Gramlich and Lucas in 2006, whether level-decreasingness can be dropped from their preservation of confluence result, in the affirmative, partially. We moreover answer their second open problem, asking whether confluence in the limit holds under mild assumptions, in the affirmative. We consider both the potentially and actually infinite cases, of infinite reductions on finite terms respectively of strongly convergent reductions from finite to (possibly) infinite terms.