YES TRS: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} DP: Strict: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} EDG: {(f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))) (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))) (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x))))) (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(b(), x)) (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(x, y)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), x)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x))))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))) (f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x)), f#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))} SCCS: Scc: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))} SCC: Strict: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(b(), x), f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} POLY: Argument Filtering: pi(c) = [], pi(a) = [], pi(b) = [], pi(f#) = 0, pi(f) = 0 Usable Rules: {} Interpretation: [c] = 0, [a] = 1, [b] = 0 Strict: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} EDG: {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y)) (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y)) (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(x, f(y, z)) -> f#(x, y), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))) (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(x, f(y, z)) -> f#(x, y)) (f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))), f#(x, f(y, z)) -> f#(f(x, y), z))} SCCS: Scc: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} SCC: Strict: { f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} UR: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} BOUND: Bound: match(-raise)-DP-bounded by 0 Automaton: { d_0() -> 5* c_0() -> 3* a_0() -> 2* b_0() -> 4* f#_0(9, 5) -> 1* f#_0(8, 6) -> 1* f#_0(8, 4) -> 1* f#_0(2, 10) -> 1* f#_0(2, 7) -> 1* f#_0(2, 3) -> 1* f_0(10, 5) -> 7* f_0(9, 5) -> 9* f_0(8, 6) -> 9* f_0(8, 4) -> 9* f_0(7, 5) -> 7* f_0(6, 5) -> 6* f_0(4, 5) -> 6* f_0(3, 6) -> 7* f_0(3, 4) -> 10* f_0(2, 10) -> 9* f_0(2, 7) -> 9* f_0(2, 3) -> 8*} Strict: {f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z)} EDG: {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(x, y)) (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(x, y)) (f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z))} SCCS: Scc: {f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z)} SCC: Strict: {f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z)} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} SPSC: Simple Projection: pi(f#) = 1 Strict: {f#(x, f(y, z)) -> f#(f(x, y), z)} EDG: {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z))} SCCS: Scc: {f#(x, f(y, z)) -> f#(f(x, y), z)} SCC: Strict: {f#(x, f(y, z)) -> f#(f(x, y), z)} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(f(a(), b()), c()), x) -> f(b(), f(a(), f(c(), f(b(), x))))} SPSC: Simple Projection: pi(f#) = 1 Strict: {} Qed