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