  There are many evaluation strategies for term rewrite systems, but proving
termination automatically is usually easiest for innermost rewriting. Several
syntactic criteria exist when innermost termination implies full termination.
We adapt these criteria to the probabilistic setting, e.g., we show when it
suffices to analyze almost-sure termination (AST) w.r.t. innermost rewriting to
prove full AST of probabilistic term rewrite systems (PTRSs). These criteria
also apply to other notions of termination like positive AST. We implemented
and evaluated our new contributions in the tool AProVE.
