Elimination of Conditions

We formally define and prove the correctness of a transformation from conditional rewrite systems (CTRS) into unconditional ones. The main result states that this transformation applies to any kind of CTRS (including extra variables in conditions) without any restrictions, and that derivations are preserved up to a mapping between terms. We also prove that termination and confluence of the original system are preserved in the transformed one under some natural assumptions.