MAYBE Time: 0.064585 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: DP: { norm# g(x, y) -> norm# x, f#(x, g(y, z)) -> f#(x, y), rem#(g(x, y), s z) -> rem#(x, z)} 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)} EDG: {(rem#(g(x, y), s z) -> rem#(x, z), rem#(g(x, y), s z) -> rem#(x, z)) (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)} STATUS: arrows: 0.666667 SCCS (3): Scc: {f#(x, g(y, z)) -> f#(x, y)} Scc: {rem#(g(x, y), s z) -> rem#(x, z)} Scc: {norm# g(x, y) -> norm# x} SCC (1): 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)} Open SCC (1): 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)} Open SCC (1): 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)} Open