YES TRS: { a(y, x) -> y, a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()), b(x, y) -> c(a(c(y), a(0(), x)))} DP: Strict: {a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x), a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()), a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y), b#(x, y) -> a#(c(y), a(0(), x)), b#(x, y) -> a#(0(), x)} Weak: { a(y, x) -> y, a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()), b(x, y) -> c(a(c(y), a(0(), x)))} EDG: {(a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()), b#(x, y) -> a#(0(), x)) (a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()), b#(x, y) -> a#(c(y), a(0(), x))) (b#(x, y) -> a#(c(y), a(0(), x)), a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y)) (b#(x, y) -> a#(c(y), a(0(), x)), a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0())) (b#(x, y) -> a#(c(y), a(0(), x)), a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x)) (a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x), a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x)) (a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x), a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0())) (a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x), a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y)) (a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y), b#(x, y) -> a#(c(y), a(0(), x))) (a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y), b#(x, y) -> a#(0(), x)) (b#(x, y) -> a#(0(), x), a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x)) (b#(x, y) -> a#(0(), x), a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0())) (b#(x, y) -> a#(0(), x), a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y))} SCCS: Scc: {a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x), a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()), a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y), b#(x, y) -> a#(c(y), a(0(), x)), b#(x, y) -> a#(0(), x)} SCC: Strict: {a#(y, c(b(a(0(), x), 0()))) -> a#(c(b(0(), y)), x), a#(y, c(b(a(0(), x), 0()))) -> b#(a(c(b(0(), y)), x), 0()), a#(y, c(b(a(0(), x), 0()))) -> b#(0(), y), b#(x, y) -> a#(c(y), a(0(), x)), b#(x, y) -> a#(0(), x)} Weak: { a(y, x) -> y, a(y, c(b(a(0(), x), 0()))) -> b(a(c(b(0(), y)), x), 0()), b(x, y) -> c(a(c(y), a(0(), x)))} BOUND: Bound: match(-raise)-bounded by 2 Automaton: { b#_1(13, 7) -> 3* b#_1(9, 7) -> 6* b#_1(7, 11) -> 3* b#_1(7, 7) -> 6* b#_1(7, 2) -> 3* b#_1(7, 1) -> 3* b#_0(6, 6) -> 6* b#_0(6, 5) -> 6* b#_0(6, 4) -> 6* b#_0(6, 3) -> 6* b#_0(6, 2) -> 6* b#_0(6, 1) -> 6* b#_0(5, 6) -> 6* b#_0(5, 5) -> 6* b#_0(5, 4) -> 6* b#_0(5, 3) -> 6* b#_0(5, 2) -> 6* b#_0(5, 1) -> 6* b#_0(4, 6) -> 6* b#_0(4, 5) -> 6* b#_0(4, 4) -> 6* b#_0(4, 3) -> 6* b#_0(4, 2) -> 6* b#_0(4, 1) -> 6* b#_0(3, 6) -> 6* b#_0(3, 5) -> 6* b#_0(3, 4) -> 6* b#_0(3, 3) -> 6* b#_0(3, 2) -> 6* b#_0(3, 1) -> 6* b#_0(2, 6) -> 6* b#_0(2, 5) -> 6* b#_0(2, 4) -> 6* b#_0(2, 3) -> 6* b#_0(2, 2) -> 6* b#_0(2, 1) -> 6* b#_0(1, 6) -> 6* b#_0(1, 5) -> 6* b#_0(1, 4) -> 6* b#_0(1, 3) -> 6* b#_0(1, 2) -> 6* b#_0(1, 1) -> 6* b_1(13, 7) -> 13 | 2 b_1(9, 7) -> 9* b_1(7, 11) -> 10* b_1(7, 7) -> 15* b_1(7, 2) -> 10* b_1(7, 1) -> 10* b_0(6, 6) -> 5* b_0(6, 5) -> 5* b_0(6, 4) -> 5* b_0(6, 3) -> 5* b_0(6, 2) -> 5* b_0(6, 1) -> 5* b_0(5, 6) -> 5* b_0(5, 5) -> 5* b_0(5, 4) -> 5* b_0(5, 3) -> 5* b_0(5, 2) -> 5* b_0(5, 1) -> 5* b_0(4, 6) -> 5* b_0(4, 5) -> 5* b_0(4, 4) -> 5* b_0(4, 3) -> 5* b_0(4, 2) -> 5* b_0(4, 1) -> 5* b_0(3, 6) -> 5* b_0(3, 5) -> 5* b_0(3, 4) -> 5* b_0(3, 3) -> 5* b_0(3, 2) -> 5* b_0(3, 1) -> 5* b_0(2, 6) -> 5* b_0(2, 5) -> 5* b_0(2, 4) -> 5* b_0(2, 3) -> 5* b_0(2, 2) -> 5* b_0(2, 1) -> 5* b_0(1, 6) -> 5* b_0(1, 5) -> 5* b_0(1, 4) -> 5* b_0(1, 3) -> 5* b_0(1, 2) -> 5* b_0(1, 1) -> 5* 0_2() -> 14* 0_1() -> 7* 0_0() -> 4* a#_2(18, 19) -> 3* a#_2(18, 17) -> 6* a#_2(16, 17) -> 3* a#_2(14, 13) -> 3* a#_2(14, 9) -> 6* a#_2(14, 7) -> 6 | 3 a#_1(11, 2) -> 3* a#_1(11, 1) -> 3* a#_1(8, 9) -> 6* a#_1(7, 2) -> 6* a#_1(7, 1) -> 6* a#_0(6, 6) -> 3* a#_0(6, 5) -> 3* a#_0(6, 4) -> 3* a#_0(6, 3) -> 3* a#_0(6, 2) -> 3* a#_0(6, 1) -> 3* a#_0(5, 6) -> 3* a#_0(5, 5) -> 3* a#_0(5, 4) -> 3* a#_0(5, 3) -> 3* a#_0(5, 2) -> 3* a#_0(5, 1) -> 3* a#_0(4, 6) -> 3* a#_0(4, 5) -> 3* a#_0(4, 4) -> 3* a#_0(4, 3) -> 3* a#_0(4, 2) -> 3* a#_0(4, 1) -> 3* a#_0(3, 6) -> 3* a#_0(3, 5) -> 3* a#_0(3, 4) -> 3* a#_0(3, 3) -> 3* a#_0(3, 2) -> 3* a#_0(3, 1) -> 3* a#_0(2, 6) -> 3* a#_0(2, 5) -> 3* a#_0(2, 4) -> 3* a#_0(2, 3) -> 3* a#_0(2, 2) -> 3* a#_0(2, 1) -> 3* a#_0(1, 6) -> 3* a#_0(1, 5) -> 3* a#_0(1, 4) -> 3* a#_0(1, 3) -> 3* a#_0(1, 2) -> 3* a#_0(1, 1) -> 3* a_2(18, 19) -> 21* a_2(18, 17) -> 22* a_2(16, 17) -> 20* a_2(14, 13) -> 19* a_2(14, 9) -> 17* a_2(14, 7) -> 17* a_1(11, 2) -> 13* a_1(11, 1) -> 13* a_1(8, 9) -> 12* a_1(7, 2) -> 9* a_1(7, 1) -> 9* a_0(6, 6) -> 2* a_0(6, 5) -> 2* a_0(6, 4) -> 2* a_0(6, 3) -> 2* a_0(6, 2) -> 2* a_0(6, 1) -> 2* a_0(5, 6) -> 2* a_0(5, 5) -> 2* a_0(5, 4) -> 2* a_0(5, 3) -> 2* a_0(5, 2) -> 2* a_0(5, 1) -> 2* a_0(4, 6) -> 2* a_0(4, 5) -> 2* a_0(4, 4) -> 2* a_0(4, 3) -> 2* a_0(4, 2) -> 2* a_0(4, 1) -> 2* a_0(3, 6) -> 2* a_0(3, 5) -> 2* a_0(3, 4) -> 2* a_0(3, 3) -> 2* a_0(3, 2) -> 2* a_0(3, 1) -> 2* a_0(2, 6) -> 2* a_0(2, 5) -> 2* a_0(2, 4) -> 2* a_0(2, 3) -> 2* a_0(2, 2) -> 2* a_0(2, 1) -> 2* a_0(1, 6) -> 2* a_0(1, 5) -> 2* a_0(1, 4) -> 2* a_0(1, 3) -> 2* a_0(1, 2) -> 2* a_0(1, 1) -> 2* c_2(22) -> 15 | 9 c_2(21) -> 13 | 2 c_2(20) -> 10* c_2(11) -> 16* c_2(7) -> 18* c_2(2) -> 16* c_2(1) -> 16* c_1(15) -> 7* c_1(12) -> 5* c_1(10) -> 11* c_1(2) -> 8* c_1(1) -> 8* c_0(6) -> 1* c_0(5) -> 1* c_0(4) -> 1* c_0(3) -> 1* c_0(2) -> 1* c_0(1) -> 1* 18 -> 22 | 21 16 -> 20* 14 -> 19 | 17 11 -> 13* 8 -> 12* 7 -> 9* 6 -> 2* 5 -> 2* 4 -> 2* 3 -> 2* 1 -> 2*} Strict: {} Qed