Tool CaT
stdout:
MAYBE
Problem:
dx(X) -> one()
dx(a()) -> zero()
dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) -> neg(dx(ALPHA))
dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
dx(exp(ALPHA,BETA)) ->
plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA))),times
(exp(ALPHA,BETA),
times
(ln(ALPHA),dx(BETA))))
Proof:
OpenTool IRC1
stdout:
YES(?,O(n^1))
Tool IRC2
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:
{ dx(X) -> one()
, dx(a()) -> zero()
, dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA))
, dx(times(ALPHA, BETA)) ->
plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
, dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA))
, dx(neg(ALPHA)) -> neg(dx(ALPHA))
, dx(div(ALPHA, BETA)) ->
minus(div(dx(ALPHA), BETA),
times(ALPHA, div(dx(BETA), exp(BETA, two()))))
, dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)
, dx(exp(ALPHA, BETA)) ->
plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))),
times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))}
Proof Output:
'wdg' proved the best result:
Details:
--------
'wdg' succeeded with the following output:
'wdg'
-----
Answer: YES(?,O(n^1))
Input Problem: innermost runtime-complexity with respect to
Rules:
{ dx(X) -> one()
, dx(a()) -> zero()
, dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA))
, dx(times(ALPHA, BETA)) ->
plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
, dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA))
, dx(neg(ALPHA)) -> neg(dx(ALPHA))
, dx(div(ALPHA, BETA)) ->
minus(div(dx(ALPHA), BETA),
times(ALPHA, div(dx(BETA), exp(BETA, two()))))
, dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)
, dx(exp(ALPHA, BETA)) ->
plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))),
times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))}
Proof Output:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: dx^#(X) -> c_0()
, 2: dx^#(a()) -> c_1()
, 3: dx^#(plus(ALPHA, BETA)) -> c_2(dx^#(ALPHA), dx^#(BETA))
, 4: dx^#(times(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA))
, 5: dx^#(minus(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA))
, 6: dx^#(neg(ALPHA)) -> c_5(dx^#(ALPHA))
, 7: dx^#(div(ALPHA, BETA)) -> c_6(dx^#(ALPHA), dx^#(BETA))
, 8: dx^#(ln(ALPHA)) -> c_7(dx^#(ALPHA))
, 9: dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{3,9,8,7,6,5,4} [ YES(?,O(n^1)) ]
|
|->{1} [ YES(?,O(n^1)) ]
|
`->{2} [ YES(?,O(n^1)) ]
Sub-problems:
-------------
* Path {3,9,8,7,6,5,4}: 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(dx) = {}, Uargs(plus) = {}, Uargs(times) = {},
Uargs(minus) = {}, Uargs(neg) = {}, Uargs(div) = {},
Uargs(exp) = {}, Uargs(ln) = {}, Uargs(dx^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1}, Uargs(c_6) = {1, 2}, Uargs(c_7) = {1},
Uargs(c_8) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
dx(x1) = [0] x1 + [0]
one() = [0]
a() = [0]
zero() = [0]
plus(x1, x2) = [1] x1 + [1] x2 + [0]
times(x1, x2) = [1] x1 + [1] x2 + [0]
minus(x1, x2) = [1] x1 + [1] x2 + [0]
neg(x1) = [1] x1 + [0]
div(x1, x2) = [1] x1 + [1] x2 + [0]
exp(x1, x2) = [1] x1 + [1] x2 + [0]
two() = [0]
ln(x1) = [1] x1 + [0]
dx^#(x1) = [3] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules:
{ dx^#(plus(ALPHA, BETA)) -> c_2(dx^#(ALPHA), dx^#(BETA))
, dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA))
, dx^#(ln(ALPHA)) -> c_7(dx^#(ALPHA))
, dx^#(div(ALPHA, BETA)) -> c_6(dx^#(ALPHA), dx^#(BETA))
, dx^#(neg(ALPHA)) -> c_5(dx^#(ALPHA))
, dx^#(minus(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA))
, dx^#(times(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA))}
Weak Rules: {}
Proof Output:
The following argument positions are usable:
Uargs(plus) = {}, Uargs(times) = {}, Uargs(minus) = {},
Uargs(neg) = {}, Uargs(div) = {}, Uargs(exp) = {}, Uargs(ln) = {},
Uargs(dx^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1, 2},
Uargs(c_7) = {1}, Uargs(c_8) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
plus(x1, x2) = [1] x1 + [1] x2 + [4]
times(x1, x2) = [1] x1 + [1] x2 + [4]
minus(x1, x2) = [1] x1 + [1] x2 + [4]
neg(x1) = [1] x1 + [4]
div(x1, x2) = [1] x1 + [1] x2 + [2]
exp(x1, x2) = [1] x1 + [1] x2 + [4]
ln(x1) = [1] x1 + [4]
dx^#(x1) = [2] x1 + [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [7]
c_3(x1, x2) = [1] x1 + [1] x2 + [7]
c_4(x1, x2) = [1] x1 + [1] x2 + [7]
c_5(x1) = [1] x1 + [7]
c_6(x1, x2) = [1] x1 + [1] x2 + [3]
c_7(x1) = [1] x1 + [7]
c_8(x1, x2) = [1] x1 + [1] x2 + [7]
* Path {3,9,8,7,6,5,4}->{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(dx) = {}, Uargs(plus) = {}, Uargs(times) = {},
Uargs(minus) = {}, Uargs(neg) = {}, Uargs(div) = {},
Uargs(exp) = {}, Uargs(ln) = {}, Uargs(dx^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1}, Uargs(c_6) = {1, 2}, Uargs(c_7) = {1},
Uargs(c_8) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
dx(x1) = [0] x1 + [0]
one() = [0]
a() = [0]
zero() = [0]
plus(x1, x2) = [0] x1 + [0] x2 + [0]
times(x1, x2) = [0] x1 + [0] x2 + [0]
minus(x1, x2) = [0] x1 + [0] x2 + [0]
neg(x1) = [0] x1 + [0]
div(x1, x2) = [0] x1 + [0] x2 + [0]
exp(x1, x2) = [0] x1 + [0] x2 + [0]
two() = [0]
ln(x1) = [0] x1 + [0]
dx^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {dx^#(X) -> c_0()}
Weak Rules:
{ dx^#(plus(ALPHA, BETA)) -> c_2(dx^#(ALPHA), dx^#(BETA))
, dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA))
, dx^#(ln(ALPHA)) -> c_7(dx^#(ALPHA))
, dx^#(div(ALPHA, BETA)) -> c_6(dx^#(ALPHA), dx^#(BETA))
, dx^#(neg(ALPHA)) -> c_5(dx^#(ALPHA))
, dx^#(minus(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA))
, dx^#(times(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA))}
Proof Output:
The following argument positions are usable:
Uargs(plus) = {}, Uargs(times) = {}, Uargs(minus) = {},
Uargs(neg) = {}, Uargs(div) = {}, Uargs(exp) = {}, Uargs(ln) = {},
Uargs(dx^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1, 2},
Uargs(c_7) = {1}, Uargs(c_8) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
plus(x1, x2) = [1] x1 + [1] x2 + [2]
times(x1, x2) = [1] x1 + [1] x2 + [2]
minus(x1, x2) = [1] x1 + [1] x2 + [2]
neg(x1) = [1] x1 + [4]
div(x1, x2) = [1] x1 + [1] x2 + [4]
exp(x1, x2) = [1] x1 + [1] x2 + [4]
ln(x1) = [1] x1 + [4]
dx^#(x1) = [2] x1 + [1]
c_0() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
c_5(x1) = [1] x1 + [5]
c_6(x1, x2) = [1] x1 + [1] x2 + [5]
c_7(x1) = [1] x1 + [5]
c_8(x1, x2) = [1] x1 + [1] x2 + [5]
* Path {3,9,8,7,6,5,4}->{2}: 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(dx) = {}, Uargs(plus) = {}, Uargs(times) = {},
Uargs(minus) = {}, Uargs(neg) = {}, Uargs(div) = {},
Uargs(exp) = {}, Uargs(ln) = {}, Uargs(dx^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1}, Uargs(c_6) = {1, 2}, Uargs(c_7) = {1},
Uargs(c_8) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
dx(x1) = [0] x1 + [0]
one() = [0]
a() = [0]
zero() = [0]
plus(x1, x2) = [0] x1 + [0] x2 + [0]
times(x1, x2) = [0] x1 + [0] x2 + [0]
minus(x1, x2) = [0] x1 + [0] x2 + [0]
neg(x1) = [0] x1 + [0]
div(x1, x2) = [0] x1 + [0] x2 + [0]
exp(x1, x2) = [0] x1 + [0] x2 + [0]
two() = [0]
ln(x1) = [0] x1 + [0]
dx^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2) = [1] x1 + [1] x2 + [0]
c_7(x1) = [1] x1 + [0]
c_8(x1, x2) = [1] x1 + [1] x2 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: innermost DP runtime-complexity with respect to
Strict Rules: {dx^#(a()) -> c_1()}
Weak Rules:
{ dx^#(plus(ALPHA, BETA)) -> c_2(dx^#(ALPHA), dx^#(BETA))
, dx^#(exp(ALPHA, BETA)) -> c_8(dx^#(ALPHA), dx^#(BETA))
, dx^#(ln(ALPHA)) -> c_7(dx^#(ALPHA))
, dx^#(div(ALPHA, BETA)) -> c_6(dx^#(ALPHA), dx^#(BETA))
, dx^#(neg(ALPHA)) -> c_5(dx^#(ALPHA))
, dx^#(minus(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA))
, dx^#(times(ALPHA, BETA)) -> c_3(dx^#(ALPHA), dx^#(BETA))}
Proof Output:
The following argument positions are usable:
Uargs(plus) = {}, Uargs(times) = {}, Uargs(minus) = {},
Uargs(neg) = {}, Uargs(div) = {}, Uargs(exp) = {}, Uargs(ln) = {},
Uargs(dx^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {1, 2},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1, 2},
Uargs(c_7) = {1}, Uargs(c_8) = {1, 2}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
a() = [2]
plus(x1, x2) = [1] x1 + [1] x2 + [4]
times(x1, x2) = [1] x1 + [1] x2 + [2]
minus(x1, x2) = [1] x1 + [1] x2 + [2]
neg(x1) = [1] x1 + [2]
div(x1, x2) = [1] x1 + [1] x2 + [2]
exp(x1, x2) = [1] x1 + [1] x2 + [4]
ln(x1) = [1] x1 + [2]
dx^#(x1) = [2] x1 + [4]
c_1() = [1]
c_2(x1, x2) = [1] x1 + [1] x2 + [4]
c_3(x1, x2) = [1] x1 + [1] x2 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
c_5(x1) = [1] x1 + [2]
c_6(x1, x2) = [1] x1 + [1] x2 + [0]
c_7(x1) = [1] x1 + [3]
c_8(x1, x2) = [1] x1 + [1] x2 + [3]Tool RC1
stdout:
MAYBE
Tool RC2
stdout:
YES(?,O(n^1))
'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ dx(X) -> one()
, dx(a()) -> zero()
, dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA))
, dx(times(ALPHA, BETA)) ->
plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
, dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA))
, dx(neg(ALPHA)) -> neg(dx(ALPHA))
, dx(div(ALPHA, BETA)) ->
minus(div(dx(ALPHA), BETA),
times(ALPHA, div(dx(BETA), exp(BETA, two()))))
, dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)
, dx(exp(ALPHA, BETA)) ->
plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))),
times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))}
Proof Output:
'wdg' proved the best result:
Details:
--------
'wdg' succeeded with the following output:
'wdg'
-----
Answer: YES(?,O(n^1))
Input Problem: runtime-complexity with respect to
Rules:
{ dx(X) -> one()
, dx(a()) -> zero()
, dx(plus(ALPHA, BETA)) -> plus(dx(ALPHA), dx(BETA))
, dx(times(ALPHA, BETA)) ->
plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))
, dx(minus(ALPHA, BETA)) -> minus(dx(ALPHA), dx(BETA))
, dx(neg(ALPHA)) -> neg(dx(ALPHA))
, dx(div(ALPHA, BETA)) ->
minus(div(dx(ALPHA), BETA),
times(ALPHA, div(dx(BETA), exp(BETA, two()))))
, dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA)
, dx(exp(ALPHA, BETA)) ->
plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))),
times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))}
Proof Output:
Transformation Details:
-----------------------
We have computed the following set of weak (innermost) dependency pairs:
{ 1: dx^#(X) -> c_0()
, 2: dx^#(a()) -> c_1()
, 3: dx^#(plus(ALPHA, BETA)) -> c_2(dx^#(ALPHA), dx^#(BETA))
, 4: dx^#(times(ALPHA, BETA)) ->
c_3(BETA, dx^#(ALPHA), ALPHA, dx^#(BETA))
, 5: dx^#(minus(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA))
, 6: dx^#(neg(ALPHA)) -> c_5(dx^#(ALPHA))
, 7: dx^#(div(ALPHA, BETA)) ->
c_6(dx^#(ALPHA), BETA, ALPHA, dx^#(BETA), BETA)
, 8: dx^#(ln(ALPHA)) -> c_7(dx^#(ALPHA), ALPHA)
, 9: dx^#(exp(ALPHA, BETA)) ->
c_8(BETA,
ALPHA,
BETA,
dx^#(ALPHA),
ALPHA,
BETA,
ALPHA,
dx^#(BETA))}
Following Dependency Graph (modulo SCCs) was computed. (Answers to
subproofs are indicated to the right.)
->{3,9,8,7,6,5,4} [ YES(?,O(n^1)) ]
|
|->{1} [ YES(?,O(n^1)) ]
|
`->{2} [ YES(?,O(n^1)) ]
Sub-problems:
-------------
* Path {3,9,8,7,6,5,4}: 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(dx) = {}, Uargs(plus) = {}, Uargs(times) = {},
Uargs(minus) = {}, Uargs(neg) = {}, Uargs(div) = {},
Uargs(exp) = {}, Uargs(ln) = {}, Uargs(dx^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1}, Uargs(c_6) = {1, 4}, Uargs(c_7) = {1},
Uargs(c_8) = {4, 8}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
dx(x1) = [0] x1 + [0]
one() = [0]
a() = [0]
zero() = [0]
plus(x1, x2) = [1] x1 + [1] x2 + [0]
times(x1, x2) = [1] x1 + [1] x2 + [0]
minus(x1, x2) = [1] x1 + [1] x2 + [0]
neg(x1) = [1] x1 + [0]
div(x1, x2) = [1] x1 + [1] x2 + [0]
exp(x1, x2) = [1] x1 + [1] x2 + [0]
two() = [0]
ln(x1) = [1] x1 + [0]
dx^#(x1) = [3] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2, x3, x4, x5) = [1] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [0]
c_7(x1, x2) = [1] x1 + [0] x2 + [0]
c_8(x1, x2, x3, x4, x5, x6, x7, x8) = [0] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [0] x6 + [0] x7 + [1] x8 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: DP runtime-complexity with respect to
Strict Rules:
{ dx^#(plus(ALPHA, BETA)) -> c_2(dx^#(ALPHA), dx^#(BETA))
, dx^#(exp(ALPHA, BETA)) ->
c_8(BETA, ALPHA, BETA, dx^#(ALPHA), ALPHA, BETA, ALPHA, dx^#(BETA))
, dx^#(ln(ALPHA)) -> c_7(dx^#(ALPHA), ALPHA)
, dx^#(div(ALPHA, BETA)) ->
c_6(dx^#(ALPHA), BETA, ALPHA, dx^#(BETA), BETA)
, dx^#(neg(ALPHA)) -> c_5(dx^#(ALPHA))
, dx^#(minus(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA))
, dx^#(times(ALPHA, BETA)) ->
c_3(BETA, dx^#(ALPHA), ALPHA, dx^#(BETA))}
Weak Rules: {}
Proof Output:
The following argument positions are usable:
Uargs(plus) = {}, Uargs(times) = {}, Uargs(minus) = {},
Uargs(neg) = {}, Uargs(div) = {}, Uargs(exp) = {}, Uargs(ln) = {},
Uargs(dx^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1, 4},
Uargs(c_7) = {1}, Uargs(c_8) = {4, 8}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
plus(x1, x2) = [1] x1 + [1] x2 + [2]
times(x1, x2) = [1] x1 + [1] x2 + [4]
minus(x1, x2) = [1] x1 + [1] x2 + [1]
neg(x1) = [1] x1 + [4]
div(x1, x2) = [1] x1 + [1] x2 + [4]
exp(x1, x2) = [1] x1 + [1] x2 + [4]
ln(x1) = [1] x1 + [4]
dx^#(x1) = [2] x1 + [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [3]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [7]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [7]
c_6(x1, x2, x3, x4, x5) = [1] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [7]
c_7(x1, x2) = [1] x1 + [0] x2 + [7]
c_8(x1, x2, x3, x4, x5, x6, x7, x8) = [0] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [0] x6 + [0] x7 + [1] x8 + [7]
* Path {3,9,8,7,6,5,4}->{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(dx) = {}, Uargs(plus) = {}, Uargs(times) = {},
Uargs(minus) = {}, Uargs(neg) = {}, Uargs(div) = {},
Uargs(exp) = {}, Uargs(ln) = {}, Uargs(dx^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1}, Uargs(c_6) = {1, 4}, Uargs(c_7) = {1},
Uargs(c_8) = {4, 8}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
dx(x1) = [0] x1 + [0]
one() = [0]
a() = [0]
zero() = [0]
plus(x1, x2) = [0] x1 + [0] x2 + [0]
times(x1, x2) = [0] x1 + [0] x2 + [0]
minus(x1, x2) = [0] x1 + [0] x2 + [0]
neg(x1) = [0] x1 + [0]
div(x1, x2) = [0] x1 + [0] x2 + [0]
exp(x1, x2) = [0] x1 + [0] x2 + [0]
two() = [0]
ln(x1) = [0] x1 + [0]
dx^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2, x3, x4, x5) = [1] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [0]
c_7(x1, x2) = [1] x1 + [0] x2 + [0]
c_8(x1, x2, x3, x4, x5, x6, x7, x8) = [0] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [0] x6 + [0] x7 + [1] x8 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: DP runtime-complexity with respect to
Strict Rules: {dx^#(X) -> c_0()}
Weak Rules:
{ dx^#(plus(ALPHA, BETA)) -> c_2(dx^#(ALPHA), dx^#(BETA))
, dx^#(exp(ALPHA, BETA)) ->
c_8(BETA, ALPHA, BETA, dx^#(ALPHA), ALPHA, BETA, ALPHA, dx^#(BETA))
, dx^#(ln(ALPHA)) -> c_7(dx^#(ALPHA), ALPHA)
, dx^#(div(ALPHA, BETA)) ->
c_6(dx^#(ALPHA), BETA, ALPHA, dx^#(BETA), BETA)
, dx^#(neg(ALPHA)) -> c_5(dx^#(ALPHA))
, dx^#(minus(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA))
, dx^#(times(ALPHA, BETA)) ->
c_3(BETA, dx^#(ALPHA), ALPHA, dx^#(BETA))}
Proof Output:
The following argument positions are usable:
Uargs(plus) = {}, Uargs(times) = {}, Uargs(minus) = {},
Uargs(neg) = {}, Uargs(div) = {}, Uargs(exp) = {}, Uargs(ln) = {},
Uargs(dx^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1, 4},
Uargs(c_7) = {1}, Uargs(c_8) = {4, 8}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
plus(x1, x2) = [1] x1 + [1] x2 + [4]
times(x1, x2) = [1] x1 + [1] x2 + [2]
minus(x1, x2) = [1] x1 + [1] x2 + [4]
neg(x1) = [1] x1 + [4]
div(x1, x2) = [1] x1 + [1] x2 + [2]
exp(x1, x2) = [1] x1 + [1] x2 + [2]
ln(x1) = [1] x1 + [4]
dx^#(x1) = [2] x1 + [1]
c_0() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [5]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [1]
c_4(x1, x2) = [1] x1 + [1] x2 + [4]
c_5(x1) = [1] x1 + [1]
c_6(x1, x2, x3, x4, x5) = [1] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [1]
c_7(x1, x2) = [1] x1 + [0] x2 + [2]
c_8(x1, x2, x3, x4, x5, x6, x7, x8) = [0] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [0] x6 + [0] x7 + [1] x8 + [1]
* Path {3,9,8,7,6,5,4}->{2}: 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(dx) = {}, Uargs(plus) = {}, Uargs(times) = {},
Uargs(minus) = {}, Uargs(neg) = {}, Uargs(div) = {},
Uargs(exp) = {}, Uargs(ln) = {}, Uargs(dx^#) = {},
Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4}, Uargs(c_4) = {1, 2},
Uargs(c_5) = {1}, Uargs(c_6) = {1, 4}, Uargs(c_7) = {1},
Uargs(c_8) = {4, 8}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
dx(x1) = [0] x1 + [0]
one() = [0]
a() = [0]
zero() = [0]
plus(x1, x2) = [0] x1 + [0] x2 + [0]
times(x1, x2) = [0] x1 + [0] x2 + [0]
minus(x1, x2) = [0] x1 + [0] x2 + [0]
neg(x1) = [0] x1 + [0]
div(x1, x2) = [0] x1 + [0] x2 + [0]
exp(x1, x2) = [0] x1 + [0] x2 + [0]
two() = [0]
ln(x1) = [0] x1 + [0]
dx^#(x1) = [0] x1 + [0]
c_0() = [0]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [0]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [0]
c_4(x1, x2) = [1] x1 + [1] x2 + [0]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2, x3, x4, x5) = [1] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [0]
c_7(x1, x2) = [1] x1 + [0] x2 + [0]
c_8(x1, x2, x3, x4, x5, x6, x7, x8) = [0] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [0] x6 + [0] x7 + [1] x8 + [0]
We apply the sub-processor on the resulting sub-problem:
'matrix-interpretation of dimension 1'
--------------------------------------
Answer: YES(?,O(n^1))
Input Problem: DP runtime-complexity with respect to
Strict Rules: {dx^#(a()) -> c_1()}
Weak Rules:
{ dx^#(plus(ALPHA, BETA)) -> c_2(dx^#(ALPHA), dx^#(BETA))
, dx^#(exp(ALPHA, BETA)) ->
c_8(BETA, ALPHA, BETA, dx^#(ALPHA), ALPHA, BETA, ALPHA, dx^#(BETA))
, dx^#(ln(ALPHA)) -> c_7(dx^#(ALPHA), ALPHA)
, dx^#(div(ALPHA, BETA)) ->
c_6(dx^#(ALPHA), BETA, ALPHA, dx^#(BETA), BETA)
, dx^#(neg(ALPHA)) -> c_5(dx^#(ALPHA))
, dx^#(minus(ALPHA, BETA)) -> c_4(dx^#(ALPHA), dx^#(BETA))
, dx^#(times(ALPHA, BETA)) ->
c_3(BETA, dx^#(ALPHA), ALPHA, dx^#(BETA))}
Proof Output:
The following argument positions are usable:
Uargs(plus) = {}, Uargs(times) = {}, Uargs(minus) = {},
Uargs(neg) = {}, Uargs(div) = {}, Uargs(exp) = {}, Uargs(ln) = {},
Uargs(dx^#) = {}, Uargs(c_2) = {1, 2}, Uargs(c_3) = {2, 4},
Uargs(c_4) = {1, 2}, Uargs(c_5) = {1}, Uargs(c_6) = {1, 4},
Uargs(c_7) = {1}, Uargs(c_8) = {4, 8}
We have the following constructor-restricted matrix interpretation:
Interpretation Functions:
a() = [0]
plus(x1, x2) = [1] x1 + [1] x2 + [2]
times(x1, x2) = [1] x1 + [1] x2 + [2]
minus(x1, x2) = [1] x1 + [1] x2 + [2]
neg(x1) = [1] x1 + [0]
div(x1, x2) = [1] x1 + [1] x2 + [4]
exp(x1, x2) = [1] x1 + [1] x2 + [2]
ln(x1) = [1] x1 + [2]
dx^#(x1) = [2] x1 + [1]
c_1() = [0]
c_2(x1, x2) = [1] x1 + [1] x2 + [1]
c_3(x1, x2, x3, x4) = [0] x1 + [1] x2 + [0] x3 + [1] x4 + [3]
c_4(x1, x2) = [1] x1 + [1] x2 + [1]
c_5(x1) = [1] x1 + [0]
c_6(x1, x2, x3, x4, x5) = [1] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [5]
c_7(x1, x2) = [1] x1 + [0] x2 + [1]
c_8(x1, x2, x3, x4, x5, x6, x7, x8) = [0] x1 + [0] x2 + [0] x3 + [1] x4 + [0] x5 + [0] x6 + [0] x7 + [1] x8 + [1]