Trivial


Terms allowing a trivial head-step are not normalising in weakly orthogonal term rewrite systems. Here a step s -> t is trivial if s = t.