Elimination of conditions

We formally define and prove the correctness of a transformation from condi tional rewrite systems (CTRS) into unconditional ones. The main result stat es that this transformation applies to any kind of CTRS (including extra va riables in conditions) without any restrictions, and that derivations are p reserved up to a mapping between terms. We also prove that termination and confluence of the original system are preserved in the transformed one unde r some natural assumptions. (C) 1999 Academic Press.