YES TRS: {f(a(), f(b(), f(a(), x))) -> f(a(), f(b(), f(b(), f(a(), x)))), f(b(), f(b(), f(b(), x))) -> f(b(), f(b(), x))} DP: Strict: {f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x)))), f#(a(), f(b(), f(a(), x))) -> f#(b(), f(b(), f(a(), x)))} Weak: {f(a(), f(b(), f(a(), x))) -> f(a(), f(b(), f(b(), f(a(), x)))), f(b(), f(b(), f(b(), x))) -> f(b(), f(b(), x))} EDG: {(f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x)))), f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x))))) (f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x)))), f#(a(), f(b(), f(a(), x))) -> f#(b(), f(b(), f(a(), x))))} SCCS: Scc: {f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x))))} SCC: Strict: {f#(a(), f(b(), f(a(), x))) -> f#(a(), f(b(), f(b(), f(a(), x))))} Weak: {f(a(), f(b(), f(a(), x))) -> f(a(), f(b(), f(b(), f(a(), x)))), f(b(), f(b(), f(b(), x))) -> f(b(), f(b(), x))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { b_0() -> 11* a_0() -> 10* f#_0(10, 14) -> 5* f_0(14, 14) -> 9* f_0(14, 13) -> 9* f_0(14, 12) -> 9* f_0(14, 11) -> 9* f_0(14, 10) -> 9* f_0(14, 9) -> 9* f_0(13, 14) -> 9* f_0(13, 13) -> 9* f_0(13, 12) -> 9* f_0(13, 11) -> 9* f_0(13, 10) -> 9* f_0(13, 9) -> 9* f_0(12, 14) -> 9* f_0(12, 13) -> 9* f_0(12, 12) -> 9* f_0(12, 11) -> 9* f_0(12, 10) -> 9* f_0(12, 9) -> 9* f_0(11, 14) -> 9* f_0(11, 13) -> 14 | 9 f_0(11, 12) -> 13* f_0(11, 11) -> 9* f_0(11, 10) -> 9* f_0(11, 9) -> 9* f_0(10, 14) -> 12* f_0(10, 13) -> 12* f_0(10, 12) -> 12* f_0(10, 11) -> 12* f_0(10, 10) -> 12* f_0(10, 9) -> 12* f_0(9, 14) -> 9* f_0(9, 13) -> 9* f_0(9, 12) -> 9* f_0(9, 11) -> 9* f_0(9, 10) -> 9* f_0(9, 9) -> 9*} Strict: {} Qed