YES 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)} DP: Strict: { norm#(g(x, y)) -> norm#(x), f#(x, g(y, z)) -> f#(x, y), rem#(g(x, y), s(z)) -> rem#(x, z)} Weak: { 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)} EDG: {(f#(x, g(y, z)) -> f#(x, y), f#(x, g(y, z)) -> f#(x, y)) (norm#(g(x, y)) -> norm#(x), norm#(g(x, y)) -> norm#(x)) (rem#(g(x, y), s(z)) -> rem#(x, z), rem#(g(x, y), s(z)) -> rem#(x, z))} SCCS: Scc: {rem#(g(x, y), s(z)) -> rem#(x, z)} Scc: {f#(x, g(y, z)) -> f#(x, y)} Scc: {norm#(g(x, y)) -> norm#(x)} SCC: Strict: {rem#(g(x, y), s(z)) -> rem#(x, z)} Weak: { 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)} SPSC: Simple Projection: pi(rem#) = 0 Strict: {} Qed SCC: Strict: {f#(x, g(y, z)) -> f#(x, y)} Weak: { 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)} SPSC: Simple Projection: pi(f#) = 1 Strict: {} Qed SCC: Strict: {norm#(g(x, y)) -> norm#(x)} Weak: { 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)} SPSC: Simple Projection: pi(norm#) = 0 Strict: {} Qed