YES TRS: {f(x, x) -> f(a(), b()), b() -> c()} DP: Strict: {f#(x, x) -> f#(a(), b()), f#(x, x) -> b#()} Weak: {f(x, x) -> f(a(), b()), b() -> c()} EDG: {(f#(x, x) -> f#(a(), b()), f#(x, x) -> b#()) (f#(x, x) -> f#(a(), b()), f#(x, x) -> f#(a(), b()))} SCCS: Scc: {f#(x, x) -> f#(a(), b())} SCC: Strict: {f#(x, x) -> f#(a(), b())} Weak: {f(x, x) -> f(a(), b()), b() -> c()} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { c_0() -> 3* b_0() -> 3* a_0() -> 2* f#_0(2, 3) -> 1*} Strict: {} Qed