YES TRS: {b(b(a(x))) -> a(b(b(x))), a(a(x)) -> b(b(x))} DP: Strict: {b#(b(a(x))) -> b#(x), b#(b(a(x))) -> b#(b(x)), b#(b(a(x))) -> a#(b(b(x))), a#(a(x)) -> b#(x), a#(a(x)) -> b#(b(x))} Weak: {b(b(a(x))) -> a(b(b(x))), a(a(x)) -> b(b(x))} EDG: {(a#(a(x)) -> b#(x), b#(b(a(x))) -> a#(b(b(x)))) (a#(a(x)) -> b#(x), b#(b(a(x))) -> b#(b(x))) (a#(a(x)) -> b#(x), b#(b(a(x))) -> b#(x)) (b#(b(a(x))) -> b#(b(x)), b#(b(a(x))) -> a#(b(b(x)))) (b#(b(a(x))) -> b#(b(x)), b#(b(a(x))) -> b#(b(x))) (b#(b(a(x))) -> b#(b(x)), b#(b(a(x))) -> b#(x)) (a#(a(x)) -> b#(b(x)), b#(b(a(x))) -> b#(x)) (a#(a(x)) -> b#(b(x)), b#(b(a(x))) -> b#(b(x))) (a#(a(x)) -> b#(b(x)), b#(b(a(x))) -> a#(b(b(x)))) (b#(b(a(x))) -> a#(b(b(x))), a#(a(x)) -> b#(x)) (b#(b(a(x))) -> a#(b(b(x))), a#(a(x)) -> b#(b(x))) (b#(b(a(x))) -> b#(x), b#(b(a(x))) -> b#(x)) (b#(b(a(x))) -> b#(x), b#(b(a(x))) -> b#(b(x))) (b#(b(a(x))) -> b#(x), b#(b(a(x))) -> a#(b(b(x))))} SCCS: Scc: {b#(b(a(x))) -> b#(x), b#(b(a(x))) -> b#(b(x)), b#(b(a(x))) -> a#(b(b(x))), a#(a(x)) -> b#(x), a#(a(x)) -> b#(b(x))} SCC: Strict: {b#(b(a(x))) -> b#(x), b#(b(a(x))) -> b#(b(x)), b#(b(a(x))) -> a#(b(b(x))), a#(a(x)) -> b#(x), a#(a(x)) -> b#(b(x))} Weak: {b(b(a(x))) -> a(b(b(x))), a(a(x)) -> b(b(x))} POLY: Argument Filtering: pi(a#) = 0, pi(a) = [0], pi(b#) = 0, pi(b) = 0 Usable Rules: {} Interpretation: [a](x0) = x0 + 1 Strict: {} Weak: {b(b(a(x))) -> a(b(b(x))), a(a(x)) -> b(b(x))} Qed