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)-bounded by 1 Automaton: { c_1() -> 7* | 6 | 3 c_0() -> 6* b_0() -> 3* a_0() -> 2* f#_0(2, 7) -> 4* f#_0(2, 6) -> 4* f#_0(2, 3) -> 4* f_0(2, 7) -> 1* f_0(2, 6) -> 1* f_0(2, 3) -> 1*} Strict: {} Qed