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()} UR: {b() -> c()} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { c_0() -> 9* | 7 | 6 b_0() -> 7* a_0() -> 8* f#_0(8, 9) -> 5* f#_0(8, 7) -> 5*} Strict: {} Qed