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() -> 11* | 9 | 8 b_0() -> 9* a_0() -> 10* f#_0(10, 11) -> 6* f#_0(10, 9) -> 6* f_0(11, 11) -> 7* f_0(11, 10) -> 7* f_0(11, 9) -> 7* f_0(11, 8) -> 7* f_0(11, 7) -> 7* f_0(10, 11) -> 7* f_0(10, 10) -> 7* f_0(10, 9) -> 7* f_0(10, 8) -> 7* f_0(10, 7) -> 7* f_0(9, 11) -> 7* f_0(9, 10) -> 7* f_0(9, 9) -> 7* f_0(9, 8) -> 7* f_0(9, 7) -> 7* f_0(8, 11) -> 7* f_0(8, 10) -> 7* f_0(8, 9) -> 7* f_0(8, 8) -> 7* f_0(8, 7) -> 7* f_0(7, 11) -> 7* f_0(7, 10) -> 7* f_0(7, 9) -> 7* f_0(7, 8) -> 7* f_0(7, 7) -> 7*} Strict: {} Qed