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)} POP*: Quasi-Precedence: f > g, norm > s nil ~ 0 Normal: pi(rem) = [1,2], pi(f) = [1,2], pi(norm) = [1] Safe: pi(g) = [1,2], pi(s) = [1] Predicative System: { 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;)} Qed