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