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