\subsection{Non-Termination}\label{subsec:nonterm}

nonloop: proves non-termination of some non-looping SRS