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