Tool CaT
stdout:
YES(?,O(n^2))
Problem:
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
bits(0()) -> 0()
bits(s(x)) -> s(bits(half(s(x))))
Proof:
Complexity Transformation Processor:
strict:
half(0()) -> 0()
half(s(0())) -> 0()
half(s(s(x))) -> s(half(x))
bits(0()) -> 0()
bits(s(x)) -> s(bits(half(s(x))))
weak:
Root-Labeling Processor:
strict:
half(half)(half(0)(0()())) -> half(0)(0()())
s(half)(half(0)(0()())) -> s(0)(0()())
bits(half)(half(0)(0()())) -> bits(0)(0()())
half(half)(half(s)(s(0)(0()()))) -> half(0)(0()())
s(half)(half(s)(s(0)(0()()))) -> s(0)(0()())
bits(half)(half(s)(s(0)(0()()))) -> bits(0)(0()())
half(half)(half(s)(s(s)(s(half)(x)))) -> half(s)(s(half)(half(half)(x)))
half(half)(half(s)(s(s)(s(0)(x)))) -> half(s)(s(half)(half(0)(x)))
half(half)(half(s)(s(s)(s(s)(x)))) -> half(s)(s(half)(half(s)(x)))
half(half)(half(s)(s(s)(s(bits)(x)))) -> half(s)(s(half)(half(bits)(x)))
s(half)(half(s)(s(s)(s(half)(x)))) -> s(s)(s(half)(half(half)(x)))
s(half)(half(s)(s(s)(s(0)(x)))) -> s(s)(s(half)(half(0)(x)))
s(half)(half(s)(s(s)(s(s)(x)))) -> s(s)(s(half)(half(s)(x)))
s(half)(half(s)(s(s)(s(bits)(x)))) -> s(s)(s(half)(half(bits)(x)))
bits(half)(half(s)(s(s)(s(half)(x)))) -> bits(s)(s(half)(half(half)(x)))
bits(half)(half(s)(s(s)(s(0)(x)))) -> bits(s)(s(half)(half(0)(x)))
bits(half)(half(s)(s(s)(s(s)(x)))) -> bits(s)(s(half)(half(s)(x)))
bits(half)(half(s)(s(s)(s(bits)(x)))) -> bits(s)(s(half)(half(bits)(x)))
half(bits)(bits(0)(0()())) -> half(0)(0()())
s(bits)(bits(0)(0()())) -> s(0)(0()())
bits(bits)(bits(0)(0()())) -> bits(0)(0()())
half(bits)(bits(s)(s(half)(x))) -> half(s)(s(bits)(bits(half)(half(s)(s(half)(x)))))
half(bits)(bits(s)(s(0)(x))) -> half(s)(s(bits)(bits(half)(half(s)(s(0)(x)))))
half(bits)(bits(s)(s(s)(x))) -> half(s)(s(bits)(bits(half)(half(s)(s(s)(x)))))
half(bits)(bits(s)(s(bits)(x))) -> half(s)(s(bits)(bits(half)(half(s)(s(bits)(x)))))
s(bits)(bits(s)(s(half)(x))) -> s(s)(s(bits)(bits(half)(half(s)(s(half)(x)))))
s(bits)(bits(s)(s(0)(x))) -> s(s)(s(bits)(bits(half)(half(s)(s(0)(x)))))
s(bits)(bits(s)(s(s)(x))) -> s(s)(s(bits)(bits(half)(half(s)(s(s)(x)))))
s(bits)(bits(s)(s(bits)(x))) -> s(s)(s(bits)(bits(half)(half(s)(s(bits)(x)))))
bits(bits)(bits(s)(s(half)(x))) -> bits(s)(s(bits)(bits(half)(half(s)(s(half)(x)))))
bits(bits)(bits(s)(s(0)(x))) -> bits(s)(s(bits)(bits(half)(half(s)(s(0)(x)))))
bits(bits)(bits(s)(s(s)(x))) -> bits(s)(s(bits)(bits(half)(half(s)(s(s)(x)))))
bits(bits)(bits(s)(s(bits)(x))) -> bits(s)(s(bits)(bits(half)(half(s)(s(bits)(x)))))
weak:
Matrix Interpretation Processor:
dimension: 2
max_matrix:
[1 3]
[0 1]
interpretation:
[1 3]
[bits(bits)](x0) = [0 1]x0,
[1 2] [0]
[bits(s)](x0) = [0 1]x0 + [1],
[1 2]
[half(bits)](x0) = [0 1]x0,
[1 2]
[s(bits)](x0) = [0 1]x0,
[1 1] [0]
[s(s)](x0) = [0 1]x0 + [1],
[1 1]
[half(s)](x0) = [0 1]x0,
[0]
[bits(0)](x0) = x0 + [1],
[1]
[bits(half)](x0) = x0 + [0],
[1 2] [0]
[s(0)](x0) = [0 1]x0 + [1],
[1]
[s(half)](x0) = x0 + [0],
[0]
[0()] = [3],
[1 2] [0]
[half(0)](x0) = [0 1]x0 + [1],
[1]
[half(half)](x0) = x0 + [0]
orientation:
[7] [6]
half(half)(half(0)(0()())) = [4] >= [4] = half(0)(0()())
[7] [6]
s(half)(half(0)(0()())) = [4] >= [4] = s(0)(0()())
[7] [0]
bits(half)(half(0)(0()())) = [4] >= [4] = bits(0)(0()())
[11] [6]
half(half)(half(s)(s(0)(0()()))) = [4 ] >= [4] = half(0)(0()())
[11] [6]
s(half)(half(s)(s(0)(0()()))) = [4 ] >= [4] = s(0)(0()())
[11] [0]
bits(half)(half(s)(s(0)(0()()))) = [4 ] >= [4] = bits(0)(0()())
[1 2] [3] [1 1] [2]
half(half)(half(s)(s(s)(s(half)(x)))) = [0 1]x + [1] >= [0 1]x + [0] = half(s)(s(half)(half(half)(x)))
[1 4] [4] [1 3] [2]
half(half)(half(s)(s(s)(s(0)(x)))) = [0 1]x + [2] >= [0 1]x + [1] = half(s)(s(half)(half(0)(x)))
[1 3] [4] [1 2] [1]
half(half)(half(s)(s(s)(s(s)(x)))) = [0 1]x + [2] >= [0 1]x + [0] = half(s)(s(half)(half(s)(x)))
[1 4] [2] [1 3] [1]
half(half)(half(s)(s(s)(s(bits)(x)))) = [0 1]x + [1] >= [0 1]x + [0] = half(s)(s(half)(half(bits)(x)))
[1 2] [3] [1 1] [2]
s(half)(half(s)(s(s)(s(half)(x)))) = [0 1]x + [1] >= [0 1]x + [1] = s(s)(s(half)(half(half)(x)))
[1 4] [4] [1 3] [2]
s(half)(half(s)(s(s)(s(0)(x)))) = [0 1]x + [2] >= [0 1]x + [2] = s(s)(s(half)(half(0)(x)))
[1 3] [4] [1 2] [1]
s(half)(half(s)(s(s)(s(s)(x)))) = [0 1]x + [2] >= [0 1]x + [1] = s(s)(s(half)(half(s)(x)))
[1 4] [2] [1 3] [1]
s(half)(half(s)(s(s)(s(bits)(x)))) = [0 1]x + [1] >= [0 1]x + [1] = s(s)(s(half)(half(bits)(x)))
[1 2] [3] [1 2] [2]
bits(half)(half(s)(s(s)(s(half)(x)))) = [0 1]x + [1] >= [0 1]x + [1] = bits(s)(s(half)(half(half)(x)))
[1 4] [4] [1 4] [3]
bits(half)(half(s)(s(s)(s(0)(x)))) = [0 1]x + [2] >= [0 1]x + [2] = bits(s)(s(half)(half(0)(x)))
[1 3] [4] [1 3] [1]
bits(half)(half(s)(s(s)(s(s)(x)))) = [0 1]x + [2] >= [0 1]x + [1] = bits(s)(s(half)(half(s)(x)))
[1 4] [2] [1 4] [1]
bits(half)(half(s)(s(s)(s(bits)(x)))) = [0 1]x + [1] >= [0 1]x + [1] = bits(s)(s(half)(half(bits)(x)))
[8] [6]
half(bits)(bits(0)(0()())) = [4] >= [4] = half(0)(0()())
[8] [6]
s(bits)(bits(0)(0()())) = [4] >= [4] = s(0)(0()())
[12] [0]
bits(bits)(bits(0)(0()())) = [4 ] >= [4] = bits(0)(0()())
[1 4] [3] [1 4] [2]
half(bits)(bits(s)(s(half)(x))) = [0 1]x + [1] >= [0 1]x + [0] = half(s)(s(bits)(bits(half)(half(s)(s(half)(x)))))
[1 6] [6] [1 6] [5]
half(bits)(bits(s)(s(0)(x))) = [0 1]x + [2] >= [0 1]x + [1] = half(s)(s(bits)(bits(half)(half(s)(s(0)(x)))))
[1 5] [6] [1 5] [5]
half(bits)(bits(s)(s(s)(x))) = [0 1]x + [2] >= [0 1]x + [1] = half(s)(s(bits)(bits(half)(half(s)(s(s)(x)))))
[1 6] [2] [1 6] [1]
half(bits)(bits(s)(s(bits)(x))) = [0 1]x + [1] >= [0 1]x + [0] = half(s)(s(bits)(bits(half)(half(s)(s(bits)(x)))))
[1 4] [3] [1 4] [2]
s(bits)(bits(s)(s(half)(x))) = [0 1]x + [1] >= [0 1]x + [1] = s(s)(s(bits)(bits(half)(half(s)(s(half)(x)))))
[1 6] [6] [1 6] [5]
s(bits)(bits(s)(s(0)(x))) = [0 1]x + [2] >= [0 1]x + [2] = s(s)(s(bits)(bits(half)(half(s)(s(0)(x)))))
[1 5] [6] [1 5] [5]
s(bits)(bits(s)(s(s)(x))) = [0 1]x + [2] >= [0 1]x + [2] = s(s)(s(bits)(bits(half)(half(s)(s(s)(x)))))
[1 6] [2] [1 6] [1]
s(bits)(bits(s)(s(bits)(x))) = [0 1]x + [1] >= [0 1]x + [1] = s(s)(s(bits)(bits(half)(half(s)(s(bits)(x)))))
[1 5] [4] [1 5] [2]
bits(bits)(bits(s)(s(half)(x))) = [0 1]x + [1] >= [0 1]x + [1] = bits(s)(s(bits)(bits(half)(half(s)(s(half)(x)))))
[1 7] [8] [1 7] [6]
bits(bits)(bits(s)(s(0)(x))) = [0 1]x + [2] >= [0 1]x + [2] = bits(s)(s(bits)(bits(half)(half(s)(s(0)(x)))))
[1 6] [8] [1 6] [6]
bits(bits)(bits(s)(s(s)(x))) = [0 1]x + [2] >= [0 1]x + [2] = bits(s)(s(bits)(bits(half)(half(s)(s(s)(x)))))
[1 7] [3] [1 7] [1]
bits(bits)(bits(s)(s(bits)(x))) = [0 1]x + [1] >= [0 1]x + [1] = bits(s)(s(bits)(bits(half)(half(s)(s(bits)(x)))))
problem:
strict:
weak:
half(half)(half(0)(0()())) -> half(0)(0()())
s(half)(half(0)(0()())) -> s(0)(0()())
bits(half)(half(0)(0()())) -> bits(0)(0()())
half(half)(half(s)(s(0)(0()()))) -> half(0)(0()())
s(half)(half(s)(s(0)(0()()))) -> s(0)(0()())
bits(half)(half(s)(s(0)(0()()))) -> bits(0)(0()())
half(half)(half(s)(s(s)(s(half)(x)))) -> half(s)(s(half)(half(half)(x)))
half(half)(half(s)(s(s)(s(0)(x)))) -> half(s)(s(half)(half(0)(x)))
half(half)(half(s)(s(s)(s(s)(x)))) -> half(s)(s(half)(half(s)(x)))
half(half)(half(s)(s(s)(s(bits)(x)))) -> half(s)(s(half)(half(bits)(x)))
s(half)(half(s)(s(s)(s(half)(x)))) -> s(s)(s(half)(half(half)(x)))
s(half)(half(s)(s(s)(s(0)(x)))) -> s(s)(s(half)(half(0)(x)))
s(half)(half(s)(s(s)(s(s)(x)))) -> s(s)(s(half)(half(s)(x)))
s(half)(half(s)(s(s)(s(bits)(x)))) -> s(s)(s(half)(half(bits)(x)))
bits(half)(half(s)(s(s)(s(half)(x)))) -> bits(s)(s(half)(half(half)(x)))
bits(half)(half(s)(s(s)(s(0)(x)))) -> bits(s)(s(half)(half(0)(x)))
bits(half)(half(s)(s(s)(s(s)(x)))) -> bits(s)(s(half)(half(s)(x)))
bits(half)(half(s)(s(s)(s(bits)(x)))) -> bits(s)(s(half)(half(bits)(x)))
half(bits)(bits(0)(0()())) -> half(0)(0()())
s(bits)(bits(0)(0()())) -> s(0)(0()())
bits(bits)(bits(0)(0()())) -> bits(0)(0()())
half(bits)(bits(s)(s(half)(x))) -> half(s)(s(bits)(bits(half)(half(s)(s(half)(x)))))
half(bits)(bits(s)(s(0)(x))) -> half(s)(s(bits)(bits(half)(half(s)(s(0)(x)))))
half(bits)(bits(s)(s(s)(x))) -> half(s)(s(bits)(bits(half)(half(s)(s(s)(x)))))
half(bits)(bits(s)(s(bits)(x))) -> half(s)(s(bits)(bits(half)(half(s)(s(bits)(x)))))
s(bits)(bits(s)(s(half)(x))) -> s(s)(s(bits)(bits(half)(half(s)(s(half)(x)))))
s(bits)(bits(s)(s(0)(x))) -> s(s)(s(bits)(bits(half)(half(s)(s(0)(x)))))
s(bits)(bits(s)(s(s)(x))) -> s(s)(s(bits)(bits(half)(half(s)(s(s)(x)))))
s(bits)(bits(s)(s(bits)(x))) -> s(s)(s(bits)(bits(half)(half(s)(s(bits)(x)))))
bits(bits)(bits(s)(s(half)(x))) -> bits(s)(s(bits)(bits(half)(half(s)(s(half)(x)))))
bits(bits)(bits(s)(s(0)(x))) -> bits(s)(s(bits)(bits(half)(half(s)(s(0)(x)))))
bits(bits)(bits(s)(s(s)(x))) -> bits(s)(s(bits)(bits(half)(half(s)(s(s)(x)))))
bits(bits)(bits(s)(s(bits)(x))) -> bits(s)(s(bits)(bits(half)(half(s)(s(bits)(x)))))
Qed
Tool IRC1
stdout:
YES(?,O(n^1))
Tool IRC2
stdout:
YES(?,O(n^2))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^2))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, bits(0()) -> 0()
, bits(s(x)) -> s(bits(half(s(x))))}
Proof Output:
'wdg' proved the best result:
Details:
--------
'wdg' succeeded with the following output:
'wdg'
-----
Answer: YES(?,O(n^2))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, bits(0()) -> 0()
, bits(s(x)) -> s(bits(half(s(x))))}
Proof Output:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: half^#(0()) -> c_0()
, 2: half^#(s(0())) -> c_1()
, 3: half^#(s(s(x))) -> c_2(half^#(x))
, 4: bits^#(0()) -> c_3()
, 5: bits^#(s(x)) -> c_4(bits^#(half(s(x))))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{5} [ YES(?,O(n^1)) ]
|
`->{4} [ YES(?,O(n^1)) ]
->{3} [ YES(?,O(n^1)) ]
|
|->{1} [ YES(?,O(n^1)) ]
|
`->{2} [ YES(?,O(n^2)) ]
Sub-problems:
-------------
* Path {3}: YES(?,O(n^1))
-----------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {1}, Uargs(bits^#) = {},
Uargs(c_4) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[3 3] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [1 0] x1 + [0]
[0 1] [0]
bits^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [0 0] x1 + [0]
[0 0] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {half^#(s(s(x))) -> c_2(half^#(x))}
Weak Rules: {}
Proof Output:
The following argument positions are usable:
Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_2) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
s(x1) = [1 2] x1 + [0]
[0 0] [1]
half^#(x1) = [2 2] x1 + [2]
[6 0] [0]
c_2(x1) = [1 0] x1 + [5]
[2 0] [7]
* Path {3}->{1}: YES(?,O(n^1))
----------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {1}, Uargs(bits^#) = {},
Uargs(c_4) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [1 0] x1 + [0]
[0 1] [0]
bits^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [0 0] x1 + [0]
[0 0] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {half^#(0()) -> c_0()}
Weak Rules: {half^#(s(s(x))) -> c_2(half^#(x))}
Proof Output:
The following argument positions are usable:
Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_2) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
0() = [0]
[2]
s(x1) = [1 2] x1 + [1]
[0 0] [0]
half^#(x1) = [2 2] x1 + [4]
[6 2] [0]
c_0() = [1]
[0]
c_2(x1) = [1 0] x1 + [3]
[2 0] [3]
* Path {3}->{2}: YES(?,O(n^2))
----------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {1}, Uargs(bits^#) = {},
Uargs(c_4) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [1 0] x1 + [0]
[0 1] [0]
bits^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [0 0] x1 + [0]
[0 0] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(n^2))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {half^#(s(0())) -> c_1()}
Weak Rules: {half^#(s(s(x))) -> c_2(half^#(x))}
Proof Output:
The following argument positions are usable:
Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_2) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
0() = [1]
[0]
s(x1) = [1 1] x1 + [2]
[0 1] [1]
half^#(x1) = [2 1] x1 + [1]
[0 0] [7]
c_1() = [1]
[1]
c_2(x1) = [1 1] x1 + [3]
[0 0] [3]
* Path {5}: YES(?,O(n^1))
-----------------------
The usable rules for this path are:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {}, Uargs(bits^#) = {1},
Uargs(c_4) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [1 2] x1 + [0]
[0 0] [2]
0() = [0]
[2]
s(x1) = [1 2] x1 + [2]
[0 0] [1]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [0 0] x1 + [0]
[0 0] [0]
bits^#(x1) = [2 0] x1 + [0]
[3 3] [0]
c_3() = [0]
[0]
c_4(x1) = [1 0] x1 + [0]
[0 1] [0]
Complexity induced by the adequate RMI: YES(?,O(n^1))
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {bits^#(s(x)) -> c_4(bits^#(half(s(x))))}
Weak Rules:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
Proof Output:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits^#) = {},
Uargs(c_4) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 1] x1 + [2]
[0 1] [0]
0() = [0]
[7]
s(x1) = [0 1] x1 + [4]
[0 1] [1]
bits^#(x1) = [1 0] x1 + [0]
[0 0] [0]
c_4(x1) = [1 0] x1 + [0]
[0 0] [0]
* Path {5}->{4}: YES(?,O(n^1))
----------------------------
The usable rules for this path are:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {1}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {}, Uargs(bits^#) = {1},
Uargs(c_4) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [2 0] x1 + [0]
[0 0] [1]
0() = [2]
[0]
s(x1) = [1 2] x1 + [0]
[0 0] [1]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [0 0] x1 + [0]
[0 0] [0]
bits^#(x1) = [3 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [1 0] x1 + [0]
[0 1] [0]
Complexity induced by the adequate RMI: YES(?,O(n^1))
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {bits^#(0()) -> c_3()}
Weak Rules:
{ bits^#(s(x)) -> c_4(bits^#(half(s(x))))
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
Proof Output:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits^#) = {},
Uargs(c_4) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
bits^#(x1) = [0 0] x1 + [1]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [1 0] x1 + [0]
[0 0] [0]Tool RC1
stdout:
YES(?,O(n^1))
Tool RC2
stdout:
YES(?,O(n^2))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^2))
Input Problem: runtime-complexity with respect to
Rules:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, bits(0()) -> 0()
, bits(s(x)) -> s(bits(half(s(x))))}
Proof Output:
'wdg' proved the best result:
Details:
--------
'wdg' succeeded with the following output:
'wdg'
-----
Answer: YES(?,O(n^2))
Input Problem: runtime-complexity with respect to
Rules:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))
, bits(0()) -> 0()
, bits(s(x)) -> s(bits(half(s(x))))}
Proof Output:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: half^#(0()) -> c_0()
, 2: half^#(s(0())) -> c_1()
, 3: half^#(s(s(x))) -> c_2(half^#(x))
, 4: bits^#(0()) -> c_3()
, 5: bits^#(s(x)) -> c_4(bits^#(half(s(x))))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{5} [ YES(?,O(n^1)) ]
|
`->{4} [ YES(?,O(n^1)) ]
->{3} [ YES(?,O(n^1)) ]
|
|->{1} [ YES(?,O(n^1)) ]
|
`->{2} [ YES(?,O(n^2)) ]
Sub-problems:
-------------
* Path {3}: YES(?,O(n^1))
-----------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {1}, Uargs(bits^#) = {},
Uargs(c_4) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [1 0] x1 + [0]
[0 0] [0]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[3 3] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [1 0] x1 + [0]
[0 1] [0]
bits^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [0 0] x1 + [0]
[0 0] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: DP runtime-complexity with respect to
Strict Rules: {half^#(s(s(x))) -> c_2(half^#(x))}
Weak Rules: {}
Proof Output:
The following argument positions are usable:
Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_2) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
s(x1) = [1 2] x1 + [0]
[0 0] [1]
half^#(x1) = [2 2] x1 + [2]
[6 0] [0]
c_2(x1) = [1 0] x1 + [5]
[2 0] [7]
* Path {3}->{1}: YES(?,O(n^1))
----------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {1}, Uargs(bits^#) = {},
Uargs(c_4) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [1 0] x1 + [0]
[0 1] [0]
bits^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [0 0] x1 + [0]
[0 0] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: DP runtime-complexity with respect to
Strict Rules: {half^#(0()) -> c_0()}
Weak Rules: {half^#(s(s(x))) -> c_2(half^#(x))}
Proof Output:
The following argument positions are usable:
Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_2) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
0() = [0]
[2]
s(x1) = [1 2] x1 + [1]
[0 0] [0]
half^#(x1) = [2 2] x1 + [4]
[6 2] [0]
c_0() = [1]
[0]
c_2(x1) = [1 0] x1 + [3]
[2 0] [3]
* Path {3}->{2}: YES(?,O(n^2))
----------------------------
The usable rules of this path are empty.
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {1}, Uargs(bits^#) = {},
Uargs(c_4) = {}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [1 0] x1 + [0]
[0 1] [0]
bits^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [0 0] x1 + [0]
[0 0] [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(n^2))
Input Problem: DP runtime-complexity with respect to
Strict Rules: {half^#(s(0())) -> c_1()}
Weak Rules: {half^#(s(s(x))) -> c_2(half^#(x))}
Proof Output:
The following argument positions are usable:
Uargs(s) = {}, Uargs(half^#) = {}, Uargs(c_2) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
0() = [1]
[0]
s(x1) = [1 1] x1 + [2]
[0 1] [1]
half^#(x1) = [2 1] x1 + [1]
[0 0] [7]
c_1() = [1]
[1]
c_2(x1) = [1 1] x1 + [3]
[0 0] [3]
* Path {5}: YES(?,O(n^1))
-----------------------
The usable rules for this path are:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {1}, Uargs(s) = {1}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {}, Uargs(bits^#) = {1},
Uargs(c_4) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [1 2] x1 + [0]
[0 0] [3]
0() = [0]
[2]
s(x1) = [1 3] x1 + [2]
[0 0] [3]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [0 0] x1 + [0]
[0 0] [0]
bits^#(x1) = [2 0] x1 + [0]
[3 3] [0]
c_3() = [0]
[0]
c_4(x1) = [1 0] x1 + [0]
[0 1] [0]
Complexity induced by the adequate RMI: YES(?,O(n^1))
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: DP runtime-complexity with respect to
Strict Rules: {bits^#(s(x)) -> c_4(bits^#(half(s(x))))}
Weak Rules:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
Proof Output:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits^#) = {},
Uargs(c_4) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 1] x1 + [2]
[0 1] [0]
0() = [0]
[7]
s(x1) = [0 1] x1 + [4]
[0 1] [1]
bits^#(x1) = [1 0] x1 + [0]
[0 0] [0]
c_4(x1) = [1 0] x1 + [0]
[0 0] [0]
* Path {5}->{4}: YES(?,O(n^1))
----------------------------
The usable rules for this path are:
{ half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
The weightgap principle applies, using the following adequate RMI:
The following argument positions are usable:
Uargs(half) = {1}, Uargs(s) = {1}, Uargs(bits) = {},
Uargs(half^#) = {}, Uargs(c_2) = {}, Uargs(bits^#) = {1},
Uargs(c_4) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [2 0] x1 + [0]
[0 0] [0]
0() = [2]
[0]
s(x1) = [1 0] x1 + [1]
[0 0] [0]
bits(x1) = [0 0] x1 + [0]
[0 0] [0]
half^#(x1) = [0 0] x1 + [0]
[0 0] [0]
c_0() = [0]
[0]
c_1() = [0]
[0]
c_2(x1) = [0 0] x1 + [0]
[0 0] [0]
bits^#(x1) = [3 0] x1 + [0]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [1 0] x1 + [0]
[0 1] [0]
Complexity induced by the adequate RMI: YES(?,O(n^1))
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 2'
--------------------------------------
Answer: YES(?,O(1))
Input Problem: DP runtime-complexity with respect to
Strict Rules: {bits^#(0()) -> c_3()}
Weak Rules:
{ bits^#(s(x)) -> c_4(bits^#(half(s(x))))
, half(0()) -> 0()
, half(s(0())) -> 0()
, half(s(s(x))) -> s(half(x))}
Proof Output:
The following argument positions are usable:
Uargs(half) = {}, Uargs(s) = {}, Uargs(bits^#) = {},
Uargs(c_4) = {1}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
half(x1) = [0 0] x1 + [0]
[0 0] [0]
0() = [0]
[0]
s(x1) = [0 0] x1 + [0]
[0 0] [0]
bits^#(x1) = [0 0] x1 + [1]
[0 0] [0]
c_3() = [0]
[0]
c_4(x1) = [1 0] x1 + [0]
[0 0] [0]