Unravelings and Ultra-properties

Conditional rewriting is universally recognized as being much more complicated than unconditional rewriting. In this paper we study how much of conditional rewriting can be automatically inferred from the simpler theory of unconditional rewriting. We introduce a new tool, called unraveling, to automatically translate a conditional term rewriting system (CTRS) into a term rewriting system (TRS). An unraveling enables to infer properties of a CTRS by studying the corresponding ultra-properties using the corresponding TRS. We show how to rediscover properties like decreasingness, and to give nice proofs of some existing results on CTRSs. Moreover, we show how unravelings provide a valuable tool to study modularity of CTRSs, automatically giving a multitude of new results