YES(?,O(n^2))
Problem:
q0(a(x1)) -> x(q1(x1))
q1(a(x1)) -> a(q1(x1))
q1(y(x1)) -> y(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
q2(x(x1)) -> x(q0(x1))
q0(y(x1)) -> y(q3(x1))
q3(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
Proof:
RT Transformation Processor:
strict:
q0(a(x1)) -> x(q1(x1))
q1(a(x1)) -> a(q1(x1))
q1(y(x1)) -> y(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
q2(x(x1)) -> x(q0(x1))
q0(y(x1)) -> y(q3(x1))
q3(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
weak:
Matrix Interpretation Processor:
dimension: 1
interpretation:
[q4](x0) = x0 + 8,
[bl](x0) = x0 + 28,
[q3](x0) = x0 + 9,
[q2](x0) = x0 + 3,
[b](x0) = x0 + 16,
[y](x0) = x0,
[x](x0) = x0 + 1,
[q1](x0) = x0,
[q0](x0) = x0 + 24,
[a](x0) = x0 + 17
orientation:
q0(a(x1)) = x1 + 41 >= x1 + 1 = x(q1(x1))
q1(a(x1)) = x1 + 17 >= x1 + 17 = a(q1(x1))
q1(y(x1)) = x1 >= x1 = y(q1(x1))
a(q1(b(x1))) = x1 + 33 >= x1 + 20 = q2(a(y(x1)))
a(q2(a(x1))) = x1 + 37 >= x1 + 37 = q2(a(a(x1)))
a(q2(y(x1))) = x1 + 20 >= x1 + 20 = q2(a(y(x1)))
y(q1(b(x1))) = x1 + 16 >= x1 + 3 = q2(y(y(x1)))
y(q2(a(x1))) = x1 + 20 >= x1 + 20 = q2(y(a(x1)))
y(q2(y(x1))) = x1 + 3 >= x1 + 3 = q2(y(y(x1)))
q2(x(x1)) = x1 + 4 >= x1 + 25 = x(q0(x1))
q0(y(x1)) = x1 + 24 >= x1 + 9 = y(q3(x1))
q3(y(x1)) = x1 + 9 >= x1 + 9 = y(q3(x1))
q3(bl(x1)) = x1 + 37 >= x1 + 36 = bl(q4(x1))
problem:
strict:
q1(a(x1)) -> a(q1(x1))
q1(y(x1)) -> y(q1(x1))
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
q2(x(x1)) -> x(q0(x1))
q3(y(x1)) -> y(q3(x1))
weak:
q0(a(x1)) -> x(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
q0(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
Matrix Interpretation Processor:
dimension: 1
interpretation:
[q4](x0) = x0,
[bl](x0) = x0 + 13,
[q3](x0) = x0 + 3,
[q2](x0) = x0 + 4,
[b](x0) = x0 + 9,
[y](x0) = x0 + 4,
[x](x0) = x0 + 2,
[q1](x0) = x0,
[q0](x0) = x0 + 3,
[a](x0) = x0 + 22
orientation:
q1(a(x1)) = x1 + 22 >= x1 + 22 = a(q1(x1))
q1(y(x1)) = x1 + 4 >= x1 + 4 = y(q1(x1))
a(q2(a(x1))) = x1 + 48 >= x1 + 48 = q2(a(a(x1)))
a(q2(y(x1))) = x1 + 30 >= x1 + 30 = q2(a(y(x1)))
y(q2(a(x1))) = x1 + 30 >= x1 + 30 = q2(y(a(x1)))
y(q2(y(x1))) = x1 + 12 >= x1 + 12 = q2(y(y(x1)))
q2(x(x1)) = x1 + 6 >= x1 + 5 = x(q0(x1))
q3(y(x1)) = x1 + 7 >= x1 + 7 = y(q3(x1))
q0(a(x1)) = x1 + 25 >= x1 + 2 = x(q1(x1))
a(q1(b(x1))) = x1 + 31 >= x1 + 30 = q2(a(y(x1)))
y(q1(b(x1))) = x1 + 13 >= x1 + 12 = q2(y(y(x1)))
q0(y(x1)) = x1 + 7 >= x1 + 7 = y(q3(x1))
q3(bl(x1)) = x1 + 16 >= x1 + 13 = bl(q4(x1))
problem:
strict:
q1(a(x1)) -> a(q1(x1))
q1(y(x1)) -> y(q1(x1))
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
q3(y(x1)) -> y(q3(x1))
weak:
q2(x(x1)) -> x(q0(x1))
q0(a(x1)) -> x(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
q0(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
Matrix Interpretation Processor:
dimension: 2
interpretation:
[1 10]
[q4](x0) = [0 0 ]x0,
[1 11] [3]
[bl](x0) = [0 0 ]x0 + [0],
[1 0]
[q3](x0) = [0 0]x0,
[0]
[q2](x0) = x0 + [2],
[1 8] [1]
[b](x0) = [0 1]x0 + [8],
[y](x0) = x0,
[1 8]
[x](x0) = [0 0]x0,
[q1](x0) = x0,
[1 6]
[q0](x0) = [0 0]x0,
[1 2]
[a](x0) = [0 1]x0
orientation:
[1 2] [1 2]
q1(a(x1)) = [0 1]x1 >= [0 1]x1 = a(q1(x1))
q1(y(x1)) = x1 >= x1 = y(q1(x1))
[1 4] [4] [1 4] [0]
a(q2(a(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(a(a(x1)))
[1 2] [4] [1 2] [0]
a(q2(y(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(a(y(x1)))
[1 2] [0] [1 2] [0]
y(q2(a(x1))) = [0 1]x1 + [2] >= [0 1]x1 + [2] = q2(y(a(x1)))
[0] [0]
y(q2(y(x1))) = x1 + [2] >= x1 + [2] = q2(y(y(x1)))
[1 0] [1 0]
q3(y(x1)) = [0 0]x1 >= [0 0]x1 = y(q3(x1))
[1 8] [0] [1 6]
q2(x(x1)) = [0 0]x1 + [2] >= [0 0]x1 = x(q0(x1))
[1 8] [1 8]
q0(a(x1)) = [0 0]x1 >= [0 0]x1 = x(q1(x1))
[1 10] [17] [1 2] [0]
a(q1(b(x1))) = [0 1 ]x1 + [8 ] >= [0 1]x1 + [2] = q2(a(y(x1)))
[1 8] [1] [0]
y(q1(b(x1))) = [0 1]x1 + [8] >= x1 + [2] = q2(y(y(x1)))
[1 6] [1 0]
q0(y(x1)) = [0 0]x1 >= [0 0]x1 = y(q3(x1))
[1 11] [3] [1 10] [3]
q3(bl(x1)) = [0 0 ]x1 + [0] >= [0 0 ]x1 + [0] = bl(q4(x1))
problem:
strict:
q1(a(x1)) -> a(q1(x1))
q1(y(x1)) -> y(q1(x1))
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
q3(y(x1)) -> y(q3(x1))
weak:
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
q2(x(x1)) -> x(q0(x1))
q0(a(x1)) -> x(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
q0(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
Matrix Interpretation Processor:
dimension: 2
interpretation:
[1 5] [13]
[q4](x0) = [0 1]x0 + [1 ],
[1 3] [2]
[bl](x0) = [0 1]x0 + [2],
[1 8] [8]
[q3](x0) = [0 1]x0 + [1],
[1 8] [0]
[q2](x0) = [0 1]x0 + [4],
[1 11] [8]
[b](x0) = [0 1 ]x0 + [5],
[1 2] [0]
[y](x0) = [0 1]x0 + [1],
[1 8] [0]
[x](x0) = [0 1]x0 + [3],
[2]
[q1](x0) = x0 + [0],
[1 8] [3]
[q0](x0) = [0 1]x0 + [2],
[1 4] [0]
[a](x0) = [0 1]x0 + [1]
orientation:
[1 4] [2] [1 4] [2]
q1(a(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = a(q1(x1))
[1 2] [2] [1 2] [2]
q1(y(x1)) = [0 1]x1 + [1] >= [0 1]x1 + [1] = y(q1(x1))
[1 14] [18] [1 14] [18]
y(q2(a(x1))) = [0 1 ]x1 + [6 ] >= [0 1 ]x1 + [6 ] = q2(y(a(x1)))
[1 12] [18] [1 12] [18]
y(q2(y(x1))) = [0 1 ]x1 + [6 ] >= [0 1 ]x1 + [6 ] = q2(y(y(x1)))
[1 10] [16] [1 10] [10]
q3(y(x1)) = [0 1 ]x1 + [2 ] >= [0 1 ]x1 + [2 ] = y(q3(x1))
[1 16] [28] [1 16] [20]
a(q2(a(x1))) = [0 1 ]x1 + [6 ] >= [0 1 ]x1 + [6 ] = q2(a(a(x1)))
[1 14] [28] [1 14] [20]
a(q2(y(x1))) = [0 1 ]x1 + [6 ] >= [0 1 ]x1 + [6 ] = q2(a(y(x1)))
[1 16] [24] [1 16] [19]
q2(x(x1)) = [0 1 ]x1 + [7 ] >= [0 1 ]x1 + [5 ] = x(q0(x1))
[1 12] [11] [1 8] [2]
q0(a(x1)) = [0 1 ]x1 + [3 ] >= [0 1]x1 + [3] = x(q1(x1))
[1 15] [30] [1 14] [20]
a(q1(b(x1))) = [0 1 ]x1 + [6 ] >= [0 1 ]x1 + [6 ] = q2(a(y(x1)))
[1 13] [20] [1 12] [18]
y(q1(b(x1))) = [0 1 ]x1 + [6 ] >= [0 1 ]x1 + [6 ] = q2(y(y(x1)))
[1 10] [11] [1 10] [10]
q0(y(x1)) = [0 1 ]x1 + [3 ] >= [0 1 ]x1 + [2 ] = y(q3(x1))
[1 11] [26] [1 8] [18]
q3(bl(x1)) = [0 1 ]x1 + [3 ] >= [0 1]x1 + [3 ] = bl(q4(x1))
problem:
strict:
q1(a(x1)) -> a(q1(x1))
q1(y(x1)) -> y(q1(x1))
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
weak:
q3(y(x1)) -> y(q3(x1))
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
q2(x(x1)) -> x(q0(x1))
q0(a(x1)) -> x(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
q0(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
Matrix Interpretation Processor:
dimension: 2
interpretation:
[1 1]
[q4](x0) = [0 0]x0,
[1 8] [4]
[bl](x0) = [0 0]x0 + [2],
[q3](x0) = x0,
[1 4] [0 ]
[q2](x0) = [0 1]x0 + [10],
[1 10] [15]
[b](x0) = [0 1 ]x0 + [12],
[1 1] [0]
[y](x0) = [0 1]x0 + [2],
[1 0] [3]
[x](x0) = [0 0]x0 + [7],
[1]
[q1](x0) = x0 + [0],
[1]
[q0](x0) = x0 + [7],
[8]
[a](x0) = x0 + [0]
orientation:
[9] [9]
q1(a(x1)) = x1 + [0] >= x1 + [0] = a(q1(x1))
[1 1] [1] [1 1] [1]
q1(y(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = y(q1(x1))
[1 5] [18] [1 5] [16]
y(q2(a(x1))) = [0 1]x1 + [12] >= [0 1]x1 + [12] = q2(y(a(x1)))
[1 6] [20] [1 6] [18]
y(q2(y(x1))) = [0 1]x1 + [14] >= [0 1]x1 + [14] = q2(y(y(x1)))
[1 1] [0] [1 1] [0]
q3(y(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = y(q3(x1))
[1 4] [16] [1 4] [16]
a(q2(a(x1))) = [0 1]x1 + [10] >= [0 1]x1 + [10] = q2(a(a(x1)))
[1 5] [16] [1 5] [16]
a(q2(y(x1))) = [0 1]x1 + [12] >= [0 1]x1 + [12] = q2(a(y(x1)))
[1 0] [31] [1 0] [4]
q2(x(x1)) = [0 0]x1 + [17] >= [0 0]x1 + [7] = x(q0(x1))
[9] [1 0] [4]
q0(a(x1)) = x1 + [7] >= [0 0]x1 + [7] = x(q1(x1))
[1 10] [24] [1 5] [16]
a(q1(b(x1))) = [0 1 ]x1 + [12] >= [0 1]x1 + [12] = q2(a(y(x1)))
[1 11] [28] [1 6] [18]
y(q1(b(x1))) = [0 1 ]x1 + [14] >= [0 1]x1 + [14] = q2(y(y(x1)))
[1 1] [1] [1 1] [0]
q0(y(x1)) = [0 1]x1 + [9] >= [0 1]x1 + [2] = y(q3(x1))
[1 8] [4] [1 1] [4]
q3(bl(x1)) = [0 0]x1 + [2] >= [0 0]x1 + [2] = bl(q4(x1))
problem:
strict:
q1(a(x1)) -> a(q1(x1))
q1(y(x1)) -> y(q1(x1))
weak:
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
q3(y(x1)) -> y(q3(x1))
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
q2(x(x1)) -> x(q0(x1))
q0(a(x1)) -> x(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
q0(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
Matrix Interpretation Processor:
dimension: 2
interpretation:
[1 12]
[q4](x0) = [0 0 ]x0,
[1 12] [5]
[bl](x0) = [0 0 ]x0 + [1],
[0]
[q3](x0) = x0 + [2],
[q2](x0) = x0,
[1 13] [3]
[b](x0) = [0 1 ]x0 + [1],
[7]
[y](x0) = x0 + [5],
[1 0]
[x](x0) = [0 0]x0,
[1 4] [1]
[q1](x0) = [0 1]x0 + [4],
[0]
[q0](x0) = x0 + [5],
[1 4] [1]
[a](x0) = [0 1]x0 + [4]
orientation:
[1 8] [18] [1 8] [18]
q1(a(x1)) = [0 1]x1 + [8 ] >= [0 1]x1 + [8 ] = a(q1(x1))
[1 4] [28] [1 4] [8]
q1(y(x1)) = [0 1]x1 + [9 ] >= [0 1]x1 + [9] = y(q1(x1))
[1 4] [8] [1 4] [8]
y(q2(a(x1))) = [0 1]x1 + [9] >= [0 1]x1 + [9] = q2(y(a(x1)))
[14] [14]
y(q2(y(x1))) = x1 + [10] >= x1 + [10] = q2(y(y(x1)))
[7] [7]
q3(y(x1)) = x1 + [7] >= x1 + [7] = y(q3(x1))
[1 8] [18] [1 8] [18]
a(q2(a(x1))) = [0 1]x1 + [8 ] >= [0 1]x1 + [8 ] = q2(a(a(x1)))
[1 4] [28] [1 4] [28]
a(q2(y(x1))) = [0 1]x1 + [9 ] >= [0 1]x1 + [9 ] = q2(a(y(x1)))
[1 0] [1 0]
q2(x(x1)) = [0 0]x1 >= [0 0]x1 = x(q0(x1))
[1 4] [1] [1 4] [1]
q0(a(x1)) = [0 1]x1 + [9] >= [0 0]x1 + [0] = x(q1(x1))
[1 21] [29] [1 4] [28]
a(q1(b(x1))) = [0 1 ]x1 + [9 ] >= [0 1]x1 + [9 ] = q2(a(y(x1)))
[1 17] [15] [14]
y(q1(b(x1))) = [0 1 ]x1 + [10] >= x1 + [10] = q2(y(y(x1)))
[7 ] [7]
q0(y(x1)) = x1 + [10] >= x1 + [7] = y(q3(x1))
[1 12] [5] [1 12] [5]
q3(bl(x1)) = [0 0 ]x1 + [3] >= [0 0 ]x1 + [1] = bl(q4(x1))
problem:
strict:
q1(a(x1)) -> a(q1(x1))
weak:
q1(y(x1)) -> y(q1(x1))
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
q3(y(x1)) -> y(q3(x1))
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
q2(x(x1)) -> x(q0(x1))
q0(a(x1)) -> x(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
q0(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
Matrix Interpretation Processor:
dimension: 2
interpretation:
[1 0]
[q4](x0) = [0 0]x0,
[1 6] [2]
[bl](x0) = [0 0]x0 + [0],
[q3](x0) = x0,
[9]
[q2](x0) = x0 + [0],
[10]
[b](x0) = x0 + [1 ],
[1 2] [0]
[y](x0) = [0 1]x0 + [8],
[1 0] [4]
[x](x0) = [0 0]x0 + [4],
[1 2] [2]
[q1](x0) = [0 1]x0 + [7],
[8]
[q0](x0) = x0 + [1],
[1 2] [0]
[a](x0) = [0 1]x0 + [8]
orientation:
[1 4] [18] [1 4] [16]
q1(a(x1)) = [0 1]x1 + [15] >= [0 1]x1 + [15] = a(q1(x1))
[1 4] [18] [1 4] [16]
q1(y(x1)) = [0 1]x1 + [15] >= [0 1]x1 + [15] = y(q1(x1))
[1 4] [25] [1 4] [25]
y(q2(a(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(y(a(x1)))
[1 4] [25] [1 4] [25]
y(q2(y(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(y(y(x1)))
[1 2] [0] [1 2] [0]
q3(y(x1)) = [0 1]x1 + [8] >= [0 1]x1 + [8] = y(q3(x1))
[1 4] [25] [1 4] [25]
a(q2(a(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(a(a(x1)))
[1 4] [25] [1 4] [25]
a(q2(y(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(a(y(x1)))
[1 0] [13] [1 0] [12]
q2(x(x1)) = [0 0]x1 + [4 ] >= [0 0]x1 + [4 ] = x(q0(x1))
[1 2] [8] [1 2] [6]
q0(a(x1)) = [0 1]x1 + [9] >= [0 0]x1 + [4] = x(q1(x1))
[1 4] [30] [1 4] [25]
a(q1(b(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(a(y(x1)))
[1 4] [30] [1 4] [25]
y(q1(b(x1))) = [0 1]x1 + [16] >= [0 1]x1 + [16] = q2(y(y(x1)))
[1 2] [8] [1 2] [0]
q0(y(x1)) = [0 1]x1 + [9] >= [0 1]x1 + [8] = y(q3(x1))
[1 6] [2] [1 0] [2]
q3(bl(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = bl(q4(x1))
problem:
strict:
weak:
q1(a(x1)) -> a(q1(x1))
q1(y(x1)) -> y(q1(x1))
y(q2(a(x1))) -> q2(y(a(x1)))
y(q2(y(x1))) -> q2(y(y(x1)))
q3(y(x1)) -> y(q3(x1))
a(q2(a(x1))) -> q2(a(a(x1)))
a(q2(y(x1))) -> q2(a(y(x1)))
q2(x(x1)) -> x(q0(x1))
q0(a(x1)) -> x(q1(x1))
a(q1(b(x1))) -> q2(a(y(x1)))
y(q1(b(x1))) -> q2(y(y(x1)))
q0(y(x1)) -> y(q3(x1))
q3(bl(x1)) -> bl(q4(x1))
Qed