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)-bounded by 3 Automaton: { d_0() -> 2* c_0() -> 7* a_0() -> 6* b_0() -> 5* f#_2(31, 8) -> 13* f#_2(31, 5) -> 13* f#_2(28, 2) -> 13* f#_2(6, 25) -> 13* f#_2(6, 7) -> 13* f#_1(31, 8) -> 13* f#_1(31, 5) -> 13* f#_1(24, 2) -> 13* f#_1(23, 8) -> 13* f#_1(23, 5) -> 13* f#_1(15, 8) -> 13* f#_1(15, 5) -> 13* f#_1(6, 25) -> 13* f#_1(6, 16) -> 13* f#_1(6, 9) -> 13* f#_1(6, 7) -> 13* f#_0(18, 2) -> 13* f#_0(15, 8) -> 13* f#_0(15, 5) -> 13* f#_0(10, 2) -> 13* f#_0(6, 16) -> 13* f#_0(6, 9) -> 13* f#_0(6, 7) -> 13* f#_0(3, 2) -> 12* f#_0(2, 2) -> 11* f_3(36, 8) -> 33 | 27 f_3(36, 5) -> 33 | 27 f_3(35, 25) -> 33 | 27 f_3(35, 7) -> 36 | 26 f_3(33, 2) -> 33 | 27 f_3(5, 31) -> 36* f_3(5, 28) -> 33* f_3(5, 6) -> 35* f_2(35, 25) -> 27* f_2(35, 7) -> 26* f_2(32, 8) -> 29* f_2(32, 5) -> 29* f_2(31, 8) -> 28 | 24 f_2(31, 5) -> 28 | 24 f_2(30, 25) -> 27 | 21 f_2(30, 16) -> 27 | 21 f_2(30, 9) -> 27 | 21 f_2(30, 7) -> 26 | 22 f_2(29, 2) -> 29 | 21 | 4 f_2(28, 2) -> 28 | 24 f_2(27, 2) -> 33 | 27 | 21 f_2(26, 8) -> 33 | 27 | 21 f_2(26, 5) -> 33 | 27 | 21 f_2(20, 25) -> 29* f_2(20, 7) -> 32* f_2(14, 25) -> 27* f_2(14, 7) -> 26* f_2(6, 25) -> 28* f_2(6, 7) -> 31* f_2(5, 31) -> 26* f_2(5, 28) -> 27* f_2(5, 24) -> 27* f_2(5, 23) -> 26* f_2(5, 15) -> 26* f_2(5, 6) -> 30* f_1(36, 8) -> 21* f_1(36, 5) -> 21* f_1(34, 2) -> 34 | 29 f_1(32, 8) -> 34* f_1(32, 5) -> 34* f_1(31, 8) -> 24* f_1(31, 5) -> 24* f_1(30, 16) -> 21* f_1(30, 9) -> 21* f_1(30, 7) -> 26* f_1(26, 8) -> 27 | 21 f_1(26, 5) -> 27 | 21 f_1(25, 2) -> 25 | 9 f_1(24, 2) -> 28 | 24 | 10 f_1(23, 8) -> 24 | 10 f_1(23, 5) -> 24 | 18 f_1(22, 8) -> 21 | 4 f_1(22, 5) -> 21 | 19 f_1(21, 2) -> 33 | 27 | 21 | 4 f_1(20, 16) -> 21 | 19 f_1(20, 9) -> 21 | 4 f_1(20, 7) -> 26 | 22 | 17 f_1(17, 8) -> 21* f_1(17, 5) -> 21* f_1(15, 8) -> 24* f_1(15, 5) -> 24* f_1(14, 25) -> 21* f_1(14, 16) -> 21* f_1(14, 9) -> 21* f_1(14, 7) -> 22* f_1(7, 8) -> 25* f_1(7, 5) -> 25* f_1(6, 25) -> 24* f_1(6, 16) -> 24* f_1(6, 9) -> 24* f_1(6, 7) -> 23* f_1(5, 24) -> 21* f_1(5, 23) -> 22* f_1(5, 18) -> 21* f_1(5, 15) -> 22* f_1(5, 10) -> 21* f_1(5, 6) -> 20* f_0(19, 2) -> 4* f_0(18, 2) -> 10* f_0(17, 8) -> 4* f_0(17, 5) -> 19* f_0(16, 2) -> 9* f_0(15, 8) -> 10* f_0(15, 5) -> 18* f_0(14, 16) -> 19* f_0(14, 9) -> 4* f_0(14, 7) -> 17* f_0(10, 2) -> 10* f_0(9, 2) -> 9* f_0(8, 2) -> 8* f_0(7, 8) -> 9* f_0(7, 5) -> 16* f_0(6, 16) -> 18* f_0(6, 9) -> 10* f_0(6, 7) -> 15* f_0(5, 18) -> 19* f_0(5, 15) -> 17* f_0(5, 10) -> 4* f_0(5, 6) -> 14* f_0(5, 2) -> 8* f_0(4, 2) -> 4* f_0(3, 2) -> 1* f_0(2, 2) -> 3* 13 -> 12 | 11 12 -> 11* 4 -> 1* 1 -> 3*} Strict: {} Qed