Tool CaT
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
Problem:
f(j(x,y),y) -> g(f(x,k(y)))
f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) -> y
i(h2(s(x),y,h1(x,z))) -> z
k(h(x)) -> h1(0(),x)
k(h1(x,y)) -> h1(s(x),y)
Proof:
Complexity Transformation Processor:
strict:
f(j(x,y),y) -> g(f(x,k(y)))
f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) -> y
i(h2(s(x),y,h1(x,z))) -> z
k(h(x)) -> h1(0(),x)
k(h1(x,y)) -> h1(s(x),y)
weak:
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[i](x0) = x0 + 14,
[h](x0) = x0 + 10,
[s](x0) = x0,
[h2](x0, x1, x2) = x0 + x1 + x2 + 5,
[0] = 9,
[h1](x0, x1) = x0 + x1 + 4,
[g](x0) = x0 + 7,
[k](x0) = x0 + 3,
[f](x0, x1) = x0 + x1 + 1,
[j](x0, x1) = x0 + x1 + 10
orientation:
f(j(x,y),y) = x + 2y + 11 >= x + y + 11 = g(f(x,k(y)))
f(x,h1(y,z)) = x + y + z + 5 >= x + y + z + 18 = h2(0(),x,h1(y,z))
g(h2(x,y,h1(z,u))) = u + x + y + z + 16 >= u + x + y + z + 9 = h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 23 >= u + x + y + z + 9 = h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) = x + y + 25 >= y = y
i(h2(s(x),y,h1(x,z))) = 2x + y + z + 23 >= z = z
k(h(x)) = x + 13 >= x + 13 = h1(0(),x)
k(h1(x,y)) = x + y + 7 >= x + y + 4 = h1(s(x),y)
problem:
strict:
f(j(x,y),y) -> g(f(x,k(y)))
f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
k(h(x)) -> h1(0(),x)
weak:
g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) -> y
i(h2(s(x),y,h1(x,z))) -> z
k(h1(x,y)) -> h1(s(x),y)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[i](x0) = x0 + 128,
[h](x0) = x0 + 1,
[s](x0) = x0 + 3,
[h2](x0, x1, x2) = x0 + x1 + x2,
[0] = 1,
[h1](x0, x1) = x0 + x1 + 65,
[g](x0) = x0 + 167,
[k](x0) = x0 + 8,
[f](x0, x1) = x0 + x1 + 128,
[j](x0, x1) = x0 + x1 + 109
orientation:
f(j(x,y),y) = x + 2y + 237 >= x + y + 303 = g(f(x,k(y)))
f(x,h1(y,z)) = x + y + z + 193 >= x + y + z + 66 = h2(0(),x,h1(y,z))
k(h(x)) = x + 9 >= x + 66 = h1(0(),x)
g(h2(x,y,h1(z,u))) = u + x + y + z + 232 >= u + x + y + z + 68 = h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 239 >= u + x + y + z + 71 = h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) = x + y + 257 >= y = y
i(h2(s(x),y,h1(x,z))) = 2x + y + z + 196 >= z = z
k(h1(x,y)) = x + y + 73 >= x + y + 68 = h1(s(x),y)
problem:
strict:
f(j(x,y),y) -> g(f(x,k(y)))
k(h(x)) -> h1(0(),x)
weak:
f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) -> y
i(h2(s(x),y,h1(x,z))) -> z
k(h1(x,y)) -> h1(s(x),y)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[i](x0) = x0,
[h](x0) = x0,
[s](x0) = x0,
[h2](x0, x1, x2) = x0 + x1 + x2,
[0] = 0,
[h1](x0, x1) = x0 + x1,
[g](x0) = x0,
[k](x0) = x0 + 1,
[f](x0, x1) = x0 + x1,
[j](x0, x1) = x0 + x1
orientation:
f(j(x,y),y) = x + 2y >= x + y + 1 = g(f(x,k(y)))
k(h(x)) = x + 1 >= x = h1(0(),x)
f(x,h1(y,z)) = x + y + z >= x + y + z = h2(0(),x,h1(y,z))
g(h2(x,y,h1(z,u))) = u + x + y + z >= u + x + y + z = h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z >= u + x + y + z = h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) = x + y >= y = y
i(h2(s(x),y,h1(x,z))) = 2x + y + z >= z = z
k(h1(x,y)) = x + y + 1 >= x + y = h1(s(x),y)
problem:
strict:
f(j(x,y),y) -> g(f(x,k(y)))
weak:
k(h(x)) -> h1(0(),x)
f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) -> y
i(h2(s(x),y,h1(x,z))) -> z
k(h1(x,y)) -> h1(s(x),y)
Matrix Interpretation Processor:
dimension: 1
max_matrix:
1
interpretation:
[i](x0) = x0,
[h](x0) = x0 + 8,
[s](x0) = x0 + 1,
[h2](x0, x1, x2) = x0 + x1 + x2 + 26,
[0] = 6,
[h1](x0, x1) = x0 + x1,
[g](x0) = x0 + 1,
[k](x0) = x0 + 4,
[f](x0, x1) = x0 + x1 + 58,
[j](x0, x1) = x0 + x1 + 6
orientation:
f(j(x,y),y) = x + 2y + 64 >= x + y + 63 = g(f(x,k(y)))
k(h(x)) = x + 12 >= x + 6 = h1(0(),x)
f(x,h1(y,z)) = x + y + z + 58 >= x + y + z + 32 = h2(0(),x,h1(y,z))
g(h2(x,y,h1(z,u))) = u + x + y + z + 27 >= u + x + y + z + 27 = h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) = 2u + x + y + 2z + 32 >= u + x + y + z + 28 = h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) = x + y + 66 >= y = y
i(h2(s(x),y,h1(x,z))) = 2x + y + z + 27 >= z = z
k(h1(x,y)) = x + y + 4 >= x + y + 1 = h1(s(x),y)
problem:
strict:
weak:
f(j(x,y),y) -> g(f(x,k(y)))
k(h(x)) -> h1(0(),x)
f(x,h1(y,z)) -> h2(0(),x,h1(y,z))
g(h2(x,y,h1(z,u))) -> h2(s(x),y,h1(z,u))
h2(x,j(y,h1(z,u)),h1(z,u)) -> h2(s(x),y,h1(s(z),u))
i(f(x,h(y))) -> y
i(h2(s(x),y,h1(x,z))) -> z
k(h1(x,y)) -> h1(s(x),y)
Qed
Tool IRC1
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
Tool IRC2
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 3
, j_0(2, 2) -> 2
, g_0(2) -> 1
, g_1(3) -> 1
, g_1(3) -> 3
, k_0(2) -> 1
, k_1(2) -> 4
, h1_0(2, 2) -> 2
, h1_1(2, 2) -> 6
, h1_1(5, 2) -> 1
, h1_1(5, 2) -> 4
, h1_2(2, 2) -> 8
, h1_2(5, 2) -> 8
, h2_0(2, 2, 2) -> 1
, h2_1(5, 2, 6) -> 1
, h2_1(5, 2, 6) -> 3
, h2_1(10, 2, 6) -> 3
, h2_2(7, 2, 8) -> 3
, h2_2(9, 2, 8) -> 1
, h2_2(9, 2, 8) -> 3
, 0_0() -> 2
, 0_1() -> 5
, 0_2() -> 7
, s_0(2) -> 2
, s_1(2) -> 2
, s_1(2) -> 5
, s_1(5) -> 5
, s_1(7) -> 10
, s_1(9) -> 5
, s_1(10) -> 5
, s_2(5) -> 9
, s_2(7) -> 9
, s_2(9) -> 9
, s_2(10) -> 9
, i_0(2) -> 1
, h_0(2) -> 2}Tool RC1
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
Tool RC2
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
Proof Output:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the best result:
Details:
--------
'Bounds with minimal-enrichment and initial automaton 'match'' succeeded with the following output:
'Bounds with minimal-enrichment and initial automaton 'match''
--------------------------------------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
Proof Output:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 3
, j_0(2, 2) -> 2
, g_0(2) -> 1
, g_1(3) -> 1
, g_1(3) -> 3
, k_0(2) -> 1
, k_1(2) -> 4
, h1_0(2, 2) -> 2
, h1_1(2, 2) -> 6
, h1_1(5, 2) -> 1
, h1_1(5, 2) -> 4
, h1_2(2, 2) -> 8
, h1_2(5, 2) -> 8
, h2_0(2, 2, 2) -> 1
, h2_1(5, 2, 6) -> 1
, h2_1(5, 2, 6) -> 3
, h2_1(10, 2, 6) -> 3
, h2_2(7, 2, 8) -> 3
, h2_2(9, 2, 8) -> 1
, h2_2(9, 2, 8) -> 3
, 0_0() -> 2
, 0_1() -> 5
, 0_2() -> 7
, s_0(2) -> 2
, s_1(2) -> 2
, s_1(2) -> 5
, s_1(5) -> 5
, s_1(7) -> 10
, s_1(9) -> 5
, s_1(10) -> 5
, s_2(5) -> 9
, s_2(7) -> 9
, s_2(9) -> 9
, s_2(10) -> 9
, i_0(2) -> 1
, h_0(2) -> 2}Tool pair1rc
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'pair1 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 3
, j_0(2, 2) -> 2
, g_0(2) -> 1
, g_1(3) -> 1
, g_1(3) -> 3
, k_0(2) -> 1
, k_1(2) -> 4
, h1_0(2, 2) -> 2
, h1_1(2, 2) -> 6
, h1_1(5, 2) -> 1
, h1_1(5, 2) -> 4
, h1_2(2, 2) -> 8
, h1_2(5, 2) -> 8
, h2_0(2, 2, 2) -> 1
, h2_1(5, 2, 6) -> 1
, h2_1(5, 2, 6) -> 3
, h2_1(10, 2, 6) -> 3
, h2_2(7, 2, 8) -> 3
, h2_2(9, 2, 8) -> 1
, h2_2(9, 2, 8) -> 3
, 0_0() -> 2
, 0_1() -> 5
, 0_2() -> 7
, s_0(2) -> 2
, s_1(2) -> 2
, s_1(2) -> 5
, s_1(5) -> 5
, s_1(7) -> 10
, s_1(9) -> 5
, s_1(10) -> 5
, s_2(5) -> 9
, s_2(7) -> 9
, s_2(9) -> 9
, s_2(10) -> 9
, i_0(2) -> 1
, h_0(2) -> 2}
Hurray, we answered YES(?,O(n^1))Tool pair2rc
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'pair2 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 3
, j_0(2, 2) -> 2
, g_0(2) -> 1
, g_1(3) -> 1
, g_1(3) -> 3
, k_0(2) -> 1
, k_1(2) -> 4
, h1_0(2, 2) -> 2
, h1_1(2, 2) -> 6
, h1_1(5, 2) -> 1
, h1_1(5, 2) -> 4
, h1_2(2, 2) -> 8
, h1_2(5, 2) -> 8
, h2_0(2, 2, 2) -> 1
, h2_1(5, 2, 6) -> 1
, h2_1(5, 2, 6) -> 3
, h2_1(10, 2, 6) -> 3
, h2_2(7, 2, 8) -> 3
, h2_2(9, 2, 8) -> 1
, h2_2(9, 2, 8) -> 3
, 0_0() -> 2
, 0_1() -> 5
, 0_2() -> 7
, s_0(2) -> 2
, s_1(2) -> 2
, s_1(2) -> 5
, s_1(5) -> 5
, s_1(7) -> 10
, s_1(9) -> 5
, s_1(10) -> 5
, s_2(5) -> 9
, s_2(7) -> 9
, s_2(9) -> 9
, s_2(10) -> 9
, i_0(2) -> 1
, h_0(2) -> 2}
Hurray, we answered YES(?,O(n^1))Tool pair3irc
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: innermost
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 3
, j_0(2, 2) -> 2
, g_0(2) -> 1
, g_1(3) -> 1
, g_1(3) -> 3
, k_0(2) -> 1
, k_1(2) -> 4
, h1_0(2, 2) -> 2
, h1_1(2, 2) -> 6
, h1_1(5, 2) -> 1
, h1_1(5, 2) -> 4
, h1_2(2, 2) -> 8
, h1_2(5, 2) -> 8
, h2_0(2, 2, 2) -> 1
, h2_1(5, 2, 6) -> 1
, h2_1(5, 2, 6) -> 3
, h2_1(10, 2, 6) -> 3
, h2_2(7, 2, 8) -> 3
, h2_2(9, 2, 8) -> 1
, h2_2(9, 2, 8) -> 3
, 0_0() -> 2
, 0_1() -> 5
, 0_2() -> 7
, s_0(2) -> 2
, s_1(2) -> 2
, s_1(2) -> 5
, s_1(5) -> 5
, s_1(7) -> 10
, s_1(9) -> 5
, s_1(10) -> 5
, s_2(5) -> 9
, s_2(7) -> 9
, s_2(9) -> 9
, s_2(10) -> 9
, i_0(2) -> 1
, h_0(2) -> 2}
Hurray, we answered YES(?,O(n^1))Tool pair3rc
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'pair3 (timeout of 60.0 seconds)':
-------------------------------------------------
The processor is not applicable, reason is:
Input problem is not restricted to innermost rewriting
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: none
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 3
, j_0(2, 2) -> 2
, g_0(2) -> 1
, g_1(3) -> 1
, g_1(3) -> 3
, k_0(2) -> 1
, k_1(2) -> 4
, h1_0(2, 2) -> 2
, h1_1(2, 2) -> 6
, h1_1(5, 2) -> 1
, h1_1(5, 2) -> 4
, h1_2(2, 2) -> 8
, h1_2(5, 2) -> 8
, h2_0(2, 2, 2) -> 1
, h2_1(5, 2, 6) -> 1
, h2_1(5, 2, 6) -> 3
, h2_1(10, 2, 6) -> 3
, h2_2(7, 2, 8) -> 3
, h2_2(9, 2, 8) -> 1
, h2_2(9, 2, 8) -> 3
, 0_0() -> 2
, 0_1() -> 5
, 0_2() -> 7
, s_0(2) -> 2
, s_1(2) -> 2
, s_1(2) -> 5
, s_1(5) -> 5
, s_1(7) -> 10
, s_1(9) -> 5
, s_1(10) -> 5
, s_2(5) -> 9
, s_2(7) -> 9
, s_2(9) -> 9
, s_2(10) -> 9
, i_0(2) -> 1
, h_0(2) -> 2}
Hurray, we answered YES(?,O(n^1))Tool rc
Execution Time | Unknown |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: none
Certificate: YES(?,O(n^1))
Application of 'rc (timeout of 60.0 seconds)':
----------------------------------------------
'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match' (timeout of 100.0 seconds)' proved the goal fastest:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 3
, j_0(2, 2) -> 2
, g_0(2) -> 1
, g_1(3) -> 1
, g_1(3) -> 3
, k_0(2) -> 1
, k_1(2) -> 4
, h1_0(2, 2) -> 2
, h1_1(2, 2) -> 6
, h1_1(5, 2) -> 1
, h1_1(5, 2) -> 4
, h1_2(2, 2) -> 8
, h1_2(5, 2) -> 8
, h2_0(2, 2, 2) -> 1
, h2_1(5, 2, 6) -> 1
, h2_1(5, 2, 6) -> 3
, h2_1(10, 2, 6) -> 3
, h2_2(7, 2, 8) -> 3
, h2_2(9, 2, 8) -> 1
, h2_2(9, 2, 8) -> 3
, 0_0() -> 2
, 0_1() -> 5
, 0_2() -> 7
, s_0(2) -> 2
, s_1(2) -> 2
, s_1(2) -> 5
, s_1(5) -> 5
, s_1(7) -> 10
, s_1(9) -> 5
, s_1(10) -> 5
, s_2(5) -> 9
, s_2(7) -> 9
, s_2(9) -> 9
, s_2(10) -> 9
, i_0(2) -> 1
, h_0(2) -> 2}
Hurray, we answered YES(?,O(n^1))Tool tup3irc
Execution Time | 0.117959976ms |
---|
Answer | YES(?,O(n^1)) |
---|
Input | SK90 2.61 |
---|
stdout:
YES(?,O(n^1))
We consider the following Problem:
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: innermost
Certificate: YES(?,O(n^1))
Application of 'tup3 (timeout of 60.0 seconds)':
------------------------------------------------
The input problem contains no overlaps that give rise to inapplicable rules.
We abort the transformation and continue with the subprocessor on the problem
Strict Trs:
{ f(j(x, y), y) -> g(f(x, k(y)))
, f(x, h1(y, z)) -> h2(0(), x, h1(y, z))
, g(h2(x, y, h1(z, u))) -> h2(s(x), y, h1(z, u))
, h2(x, j(y, h1(z, u)), h1(z, u)) -> h2(s(x), y, h1(s(z), u))
, i(f(x, h(y))) -> y
, i(h2(s(x), y, h1(x, z))) -> z
, k(h(x)) -> h1(0(), x)
, k(h1(x, y)) -> h1(s(x), y)}
StartTerms: basic terms
Strategy: innermost
1) 'Fastest' proved the goal fastest:
'Fastest' proved the goal fastest:
'Bounds with minimal-enrichment and initial automaton 'match'' proved the goal fastest:
The problem is match-bounded by 2.
The enriched problem is compatible with the following automaton:
{ f_0(2, 2) -> 1
, f_1(2, 4) -> 3
, j_0(2, 2) -> 2
, g_0(2) -> 1
, g_1(3) -> 1
, g_1(3) -> 3
, k_0(2) -> 1
, k_1(2) -> 4
, h1_0(2, 2) -> 2
, h1_1(2, 2) -> 6
, h1_1(5, 2) -> 1
, h1_1(5, 2) -> 4
, h1_2(2, 2) -> 8
, h1_2(5, 2) -> 8
, h2_0(2, 2, 2) -> 1
, h2_1(5, 2, 6) -> 1
, h2_1(5, 2, 6) -> 3
, h2_1(10, 2, 6) -> 3
, h2_2(7, 2, 8) -> 3
, h2_2(9, 2, 8) -> 1
, h2_2(9, 2, 8) -> 3
, 0_0() -> 2
, 0_1() -> 5
, 0_2() -> 7
, s_0(2) -> 2
, s_1(2) -> 2
, s_1(2) -> 5
, s_1(5) -> 5
, s_1(7) -> 10
, s_1(9) -> 5
, s_1(10) -> 5
, s_2(5) -> 9
, s_2(7) -> 9
, s_2(9) -> 9
, s_2(10) -> 9
, i_0(2) -> 1
, h_0(2) -> 2}
Hurray, we answered YES(?,O(n^1))