YES Time: 5.276315 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: DP: { 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))} 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))))} 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#(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#(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#(f(x, y), z)) (f#(f(f(a(), b()), c()), x) -> 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#(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#(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#(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 (1): 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 (6): 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0, [b] = 1, [a] = 1, [c] = 0, [f#](x0, x1) = x0 Strict: f#(f(f(a(), b()), c()), x) -> f#(c(), f(b(), x)) 1 + 0x >= 0 + 0x f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))) 1 + 0x >= 1 + 0x f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))) 1 + 0x >= 1 + 0x f#(f(f(a(), b()), c()), x) -> f#(b(), x) 1 + 0x >= 1 + 0x f#(x, f(y, z)) -> f#(f(x, y), z) 0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z f#(x, f(y, z)) -> f#(x, y) 0 + 1x + 0y + 0z >= 0 + 1x + 0y Weak: 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#(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#(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#(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#(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(), 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#(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#(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#(a(), f(c(), f(b(), x))))} SCCS (1): 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)))} SCC (5): 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)))} 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: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + x1, [b] = 0, [a] = 0, [c] = 1, [f#](x0, x1) = x0 + x1 Strict: f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))) 1 + 1x >= 1 + 1x f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))) 1 + 1x >= 1 + 1x f#(f(f(a(), b()), c()), x) -> f#(b(), x) 1 + 1x >= 0 + 1x f#(x, f(y, z)) -> f#(f(x, y), z) 0 + 1x + 1y + 1z >= 0 + 1x + 1y + 1z f#(x, f(y, z)) -> f#(x, y) 0 + 1x + 1y + 1z >= 0 + 1x + 1y Weak: 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#(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#(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#(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(), 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#(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#(b(), 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))))} SCCS (1): 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(), f(a(), f(c(), f(b(), x)))), f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x)))} SCC (4): 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(), f(a(), f(c(), f(b(), x)))), 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))))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0, [b] = 0, [a] = 1, [c] = 0, [f#](x0, x1) = x0 Strict: f#(f(f(a(), b()), c()), x) -> f#(a(), f(c(), f(b(), x))) 1 + 0x >= 1 + 0x f#(f(f(a(), b()), c()), x) -> f#(b(), f(a(), f(c(), f(b(), x)))) 1 + 0x >= 0 + 0x f#(x, f(y, z)) -> f#(f(x, y), z) 0 + 1x + 0y + 0z >= 0 + 1x + 0y + 0z f#(x, f(y, z)) -> f#(x, y) 0 + 1x + 0y + 0z >= 0 + 1x + 0y Weak: 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#(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)) (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))))} SCCS (1): 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 (3): 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))))} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { c_1() -> 16* c_0() -> 12* a_1() -> 15* a_0() -> 11* b_1() -> 17* b_0() -> 10* f#_1(21, 14) -> 6* f#_1(21, 13) -> 6* f#_1(21, 12) -> 6* f#_1(21, 11) -> 6* f#_1(21, 10) -> 6* f#_1(21, 9) -> 6* f#_1(20, 18) -> 6* f#_1(20, 17) -> 6* f#_1(15, 22) -> 6* f#_1(15, 19) -> 6* f#_1(15, 16) -> 6* f#_0(11, 14) -> 6* f#_0(11, 13) -> 6* f#_0(11, 12) -> 6* f#_0(11, 11) -> 6* f#_0(11, 10) -> 6* f#_0(11, 9) -> 6* f#_0(9, 14) -> 6* f#_0(9, 13) -> 6* f#_0(9, 12) -> 6* f#_0(9, 11) -> 6* f#_0(9, 10) -> 6* f#_0(9, 9) -> 6* f_1(22, 14) -> 19* f_1(22, 13) -> 19* f_1(22, 12) -> 19* f_1(22, 11) -> 19* f_1(22, 10) -> 19* f_1(22, 9) -> 19* f_1(21, 14) -> 21* f_1(21, 13) -> 21* f_1(21, 12) -> 21* f_1(21, 11) -> 21* f_1(21, 10) -> 21* f_1(21, 9) -> 21* f_1(20, 18) -> 21* f_1(20, 17) -> 21* f_1(19, 14) -> 19* f_1(19, 13) -> 19* f_1(19, 12) -> 19* f_1(19, 11) -> 19* f_1(19, 10) -> 19* f_1(19, 9) -> 19* f_1(18, 14) -> 18* f_1(18, 13) -> 18* f_1(18, 12) -> 18* f_1(18, 11) -> 18* f_1(18, 10) -> 18* f_1(18, 9) -> 18* f_1(17, 14) -> 18* f_1(17, 13) -> 18* f_1(17, 12) -> 18* f_1(17, 11) -> 18* f_1(17, 10) -> 18* f_1(17, 9) -> 18* f_1(16, 18) -> 19* f_1(16, 17) -> 22* f_1(15, 22) -> 21* f_1(15, 19) -> 21* f_1(15, 16) -> 20* f_0(14, 14) -> 14 | 9 f_0(14, 13) -> 14 | 9 f_0(14, 12) -> 14 | 9 f_0(14, 11) -> 14 | 9 f_0(14, 10) -> 14 | 9 f_0(14, 9) -> 14 | 9 f_0(13, 14) -> 14 | 13 | 9 f_0(13, 13) -> 14 | 13 | 9 f_0(13, 12) -> 14 | 13 | 9 f_0(13, 11) -> 14 | 13 | 9 f_0(13, 10) -> 14 | 13 | 9 f_0(13, 9) -> 14 | 13 | 9 f_0(12, 14) -> 9* f_0(12, 13) -> 14* 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) -> 9* f_0(11, 12) -> 9* f_0(11, 11) -> 9* f_0(11, 10) -> 9* f_0(11, 9) -> 9* f_0(10, 14) -> 13* f_0(10, 13) -> 13* f_0(10, 12) -> 13* f_0(10, 11) -> 13* f_0(10, 10) -> 13* f_0(10, 9) -> 14 | 13 | 9 f_0(9, 14) -> 14 | 9 f_0(9, 13) -> 14 | 9 f_0(9, 12) -> 14 | 9 f_0(9, 11) -> 14 | 9 f_0(9, 10) -> 14 | 9 f_0(9, 9) -> 14 | 9} 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 (1): Scc: {f#(x, f(y, z)) -> f#(x, y), f#(x, f(y, z)) -> f#(f(x, y), z)} SCC (2): 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 (1): Scc: {f#(x, f(y, z)) -> f#(f(x, y), z)} SCC (1): 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