Abstract
Syntactic annotations are a powerful mechanism to avoid undesired reductions. In term rewriting, Context-Sensitive Rewriting (CSR) defines the reduction relation which only rewrites the so-called active subterms, i.e., those occurring in replacing arguments of function symbols, as indicated by a replacement map $\mu$, which specifies those arguments. One of the benefits of using CSR is to model the operational behavior of the if-then-else expression in a natural way. Termination of CSR is an interesting problem with several applications in the fields of term rewriting and in the analysis of programming languages like CafeOBJ, Haskell, Maude, OBJ, etc. Direct techniques and frameworks for proving termination of CSR have been developed. But, automatic termination of context-sensitive term rewriting systems (CS-TRSs) involving if-then-else expressions is always hard in practice. In this work, we focus on how if-then-else expressions in CSR are translated into the CS-DP framework, showing why it is difficult to find a termination proof, proposing a new set of context-sensitive usable rules that allows us to simplify termination proofs in these cases and showing some examples where the technique is successfully applied.
