Loops under Strategies... Continued

Termination is an important property of term rewrite systems (TRSs). Therefore, much effort has been spent on developing and automating techniques for showing termination of TRSs. But in order to detect bugs, it is at least as important to prove non-termination of TRSs. Note that for rewriting under strategies, one cannot ignore the strategy, since a non-terminating TRS may still be terminating due to the strategy