MAYBE TRS: { f(t(), x, y) -> f(g(x, y), x, s(y)), g(s(x), s(y)) -> g(x, y), g(s(x), 0()) -> t()} DP: Strict: { f#(t(), x, y) -> f#(g(x, y), x, s(y)), f#(t(), x, y) -> g#(x, y), g#(s(x), s(y)) -> g#(x, y)} Weak: { f(t(), x, y) -> f(g(x, y), x, s(y)), g(s(x), s(y)) -> g(x, y), g(s(x), 0()) -> t()} EDG: {(f#(t(), x, y) -> g#(x, y), g#(s(x), s(y)) -> g#(x, y)) (g#(s(x), s(y)) -> g#(x, y), g#(s(x), s(y)) -> g#(x, y)) (f#(t(), x, y) -> f#(g(x, y), x, s(y)), f#(t(), x, y) -> f#(g(x, y), x, s(y))) (f#(t(), x, y) -> f#(g(x, y), x, s(y)), f#(t(), x, y) -> g#(x, y))} SCCS: Scc: {g#(s(x), s(y)) -> g#(x, y)} Scc: {f#(t(), x, y) -> f#(g(x, y), x, s(y))} SCC: Strict: {g#(s(x), s(y)) -> g#(x, y)} Weak: { f(t(), x, y) -> f(g(x, y), x, s(y)), g(s(x), s(y)) -> g(x, y), g(s(x), 0()) -> t()} SPSC: Simple Projection: pi(g#) = 0 Strict: {} Qed SCC: Strict: {f#(t(), x, y) -> f#(g(x, y), x, s(y))} Weak: { f(t(), x, y) -> f(g(x, y), x, s(y)), g(s(x), s(y)) -> g(x, y), g(s(x), 0()) -> t()} Fail