TRS: { norm(nil()) -> 0(), norm(g(x, y)) -> s(norm(x)), f(x, nil()) -> g(nil(), x), f(x, g(y, z)) -> g(f(x, y), z), rem(nil(), y) -> nil(), rem(g(x, y), 0()) -> g(x, y), rem(g(x, y), s(z)) -> rem(x, z)} MPO: Prec: g > norm, g > s, norm > 0, f > g empty Strict: {} Weak: {} Qed