YES Time: 1.420241 TRS: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(a(), f(a(), x)), f(f(b(), a()), x) -> f(b(), 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(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(f(b(), a()), x) -> f#(b(), x), f#(f(b(), a()), x) -> f#(b(), f(b(), x))} TRS: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(a(), f(a(), x)), f(f(b(), a()), x) -> f(b(), f(b(), x))} EDG: {(f#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(x, y)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), x)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), f(a(), x))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), 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(b(), a()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(b(), a()), x) -> f#(b(), x), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(a(), x), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(a(), 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(a(), b()), x) -> f#(a(), x)) (f#(x, f(y, z)) -> f#(x, y), f#(f(a(), b()), x) -> f#(a(), f(a(), x))) (f#(x, f(y, z)) -> f#(x, y), f#(f(b(), a()), x) -> f#(b(), x)) (f#(x, f(y, z)) -> f#(x, y), f#(f(b(), a()), x) -> f#(b(), f(b(), x))) (f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(a(), f(a(), 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(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(f(b(), a()), x) -> f#(b(), x), f#(f(b(), a()), x) -> f#(b(), 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(a(), b()), x) -> f#(a(), x), f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(f(b(), a()), x) -> f#(b(), x), f#(f(b(), a()), x) -> f#(b(), f(b(), x))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(a(), f(a(), x)), f(f(b(), a()), x) -> f(b(), f(b(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + x1, [a] = 1, [b] = 1, [f#](x0, x1) = x0 + x1 Strict: f#(f(b(), a()), x) -> f#(b(), f(b(), x)) 2 + 1x >= 2 + 1x f#(f(b(), a()), x) -> f#(b(), x) 2 + 1x >= 1 + 1x f#(f(a(), b()), x) -> f#(a(), f(a(), x)) 2 + 1x >= 2 + 1x f#(f(a(), b()), x) -> f#(a(), x) 2 + 1x >= 1 + 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#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(x, y)) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), f(a(), 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(a(), b()), x) -> f#(a(), f(a(), x))) (f#(x, f(y, z)) -> f#(x, y), f#(f(b(), a()), x) -> f#(b(), f(b(), x))) (f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(x, f(y, z)) -> f#(x, y)) (f#(f(a(), b()), x) -> f#(a(), f(a(), 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(a(), b()), x) -> f#(a(), f(a(), x)), f#(f(b(), a()), x) -> f#(b(), 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(a(), b()), x) -> f#(a(), f(a(), x)), f#(f(b(), a()), x) -> f#(b(), f(b(), x))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(a(), f(a(), x)), f(f(b(), a()), x) -> f(b(), f(b(), x))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + x1 + 1, [a] = 1, [b] = 1, [f#](x0, x1) = x0 + x1 Strict: f#(f(b(), a()), x) -> f#(b(), f(b(), x)) 3 + 1x >= 3 + 1x f#(f(a(), b()), x) -> f#(a(), f(a(), x)) 3 + 1x >= 3 + 1x f#(x, f(y, z)) -> f#(f(x, y), z) 1 + 1x + 1y + 1z >= 1 + 1x + 1y + 1z f#(x, f(y, z)) -> f#(x, y) 1 + 1x + 1y + 1z >= 0 + 1x + 1y Weak: EDG: {(f#(f(b(), a()), x) -> f#(b(), 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#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), f(a(), x))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x))) (f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))} SCCS (1): Scc: { f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(f(b(), a()), x) -> f#(b(), f(b(), x))} SCC (3): Strict: { f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(a(), b()), x) -> f#(a(), f(a(), x)), f#(f(b(), a()), x) -> f#(b(), f(b(), x))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(a(), f(a(), x)), f(f(b(), a()), x) -> f(b(), f(b(), x))} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { b_0() -> 9* a_1() -> 11* a_0() -> 8* f#_1(13, 12) -> 5* f#_1(13, 10) -> 5* f#_1(13, 9) -> 5* f#_1(13, 8) -> 5* f#_1(13, 7) -> 5* f#_1(11, 12) -> 5* f#_0(10, 10) -> 5* f#_0(10, 9) -> 5* f#_0(10, 8) -> 5* f#_0(10, 7) -> 5* f#_0(9, 7) -> 5* f#_0(8, 10) -> 5* f#_0(7, 10) -> 5* f#_0(7, 9) -> 5* f#_0(7, 8) -> 5* f#_0(7, 7) -> 5* f_1(13, 13) -> 13* f_1(13, 12) -> 13 | 12 f_1(13, 11) -> 13* f_1(13, 10) -> 13 | 12 f_1(13, 9) -> 13 | 12 f_1(13, 8) -> 13 | 12 f_1(13, 7) -> 13 | 12 f_1(12, 10) -> 12* f_1(12, 9) -> 12* f_1(12, 8) -> 12* f_1(12, 7) -> 12* f_1(11, 13) -> 13* f_1(11, 12) -> 13 | 12 f_1(11, 11) -> 13* f_1(11, 10) -> 12* f_1(11, 9) -> 12* f_1(11, 8) -> 12* f_1(11, 7) -> 12* f_0(10, 10) -> 10 | 7 f_0(10, 9) -> 10 | 7 f_0(10, 8) -> 10 | 7 f_0(10, 7) -> 10 | 7 f_0(9, 10) -> 7* f_0(9, 9) -> 7* f_0(9, 8) -> 7* f_0(9, 7) -> 7* f_0(8, 10) -> 10 | 7 f_0(8, 9) -> 10* f_0(8, 8) -> 10* f_0(8, 7) -> 10* f_0(7, 10) -> 7* f_0(7, 9) -> 7* f_0(7, 8) -> 7* f_0(7, 7) -> 7*} Strict: { f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x))} EDG: {(f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x))) (f#(x, f(y, z)) -> f#(f(x, y), z), f#(x, f(y, z)) -> f#(f(x, y), z)) (f#(f(b(), a()), x) -> f#(b(), f(b(), x)), f#(x, f(y, z)) -> f#(f(x, y), z))} SCCS (1): Scc: { f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x))} SCC (2): Strict: { f#(x, f(y, z)) -> f#(f(x, y), z), f#(f(b(), a()), x) -> f#(b(), f(b(), x))} Weak: { f(x, f(y, z)) -> f(f(x, y), z), f(f(a(), b()), x) -> f(a(), f(a(), x)), f(f(b(), a()), x) -> f(b(), f(b(), x))} BOUND: Bound: match(-raise)-DP-bounded by 1 Automaton: { b_1() -> 11* b_0() -> 9* a_0() -> 8* f#_1(13, 12) -> 5* f#_1(13, 10) -> 5* f#_1(13, 9) -> 5* f#_1(13, 8) -> 5* f#_1(13, 7) -> 5* f#_1(11, 12) -> 5* f#_0(10, 10) -> 5* f#_0(10, 9) -> 5* f#_0(10, 8) -> 5* f#_0(10, 7) -> 5* f#_0(9, 10) -> 5* f#_0(7, 10) -> 5* f#_0(7, 9) -> 5* f#_0(7, 8) -> 5* f#_0(7, 7) -> 5* f_1(13, 13) -> 13* f_1(13, 12) -> 13 | 12 f_1(13, 11) -> 13* f_1(13, 10) -> 13 | 12 f_1(13, 9) -> 13 | 12 f_1(13, 8) -> 13 | 12 f_1(13, 7) -> 13 | 12 f_1(12, 10) -> 12* f_1(12, 9) -> 12* f_1(12, 8) -> 12* f_1(12, 7) -> 12* f_1(11, 13) -> 13* f_1(11, 12) -> 13 | 12 f_1(11, 11) -> 13* f_1(11, 10) -> 12* f_1(11, 9) -> 12* f_1(11, 8) -> 12* f_1(11, 7) -> 12* f_0(10, 10) -> 10 | 7 f_0(10, 9) -> 10 | 7 f_0(10, 8) -> 10 | 7 f_0(10, 7) -> 10 | 7 f_0(9, 10) -> 10 | 7 f_0(9, 9) -> 10* f_0(9, 8) -> 10* f_0(9, 7) -> 10* f_0(8, 10) -> 7* f_0(8, 9) -> 7* f_0(8, 8) -> 7* f_0(8, 7) -> 7* f_0(7, 10) -> 7* f_0(7, 9) -> 7* f_0(7, 8) -> 7* f_0(7, 7) -> 7*} 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(a(), b()), x) -> f(a(), f(a(), x)), f(f(b(), a()), x) -> f(b(), f(b(), x))} SPSC: Simple Projection: pi(f#) = 1 Strict: {} Qed