Elimination of Conditions

We prove the correctness of a transformation from conditional rewrite systems (CTRS) into non conditional ones. This particular transformation has the advantage of expliciting all the possible parallelism in the evaluation of conditions. The main result states that this transformation applies to any CTRS, 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