interpretations
YES(?,O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).
Strict Trs:
{ 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(exp(ALPHA, BETA)) ->
plus(times(BETA, times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))),
times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))
, dx(ln(ALPHA)) -> div(dx(ALPHA), ALPHA) }
Obligation:
innermost runtime complexity
Answer:
YES(?,O(n^2))
The following argument positions are usable:
Uargs(dx) = {}, Uargs(plus) = {1, 2}, Uargs(times) = {2},
Uargs(minus) = {1, 2}, Uargs(neg) = {1}, Uargs(div) = {1},
Uargs(exp) = {}, Uargs(ln) = {}
TcT has computed following constructor-restricted polynomial
interpretation.
[dx](x1) = 2 + 3*x1 + 3*x1^2
[one]() = 0
[a]() = 0
[zero]() = 0
[plus](x1, x2) = 1 + x1 + x2
[times](x1, x2) = 2 + x1 + x2
[minus](x1, x2) = 1 + x1 + x2
[neg](x1) = 2 + x1
[div](x1, x2) = 3 + x1 + x2
[exp](x1, x2) = 3 + x1 + x2
[two]() = 1
[ln](x1) = 1 + x1
This order satisfies following ordering constraints
[dx(X)] = 2 + 3*X + 3*X^2
>
= [one()]
[dx(a())] = 2
>
= [zero()]
[dx(plus(ALPHA, BETA))] = 8 + 9*ALPHA + 9*BETA + 3*ALPHA^2 + 3*ALPHA*BETA + 3*BETA*ALPHA + 3*BETA^2
> 5 + 3*ALPHA + 3*ALPHA^2 + 3*BETA + 3*BETA^2
= [plus(dx(ALPHA), dx(BETA))]
[dx(times(ALPHA, BETA))] = 20 + 15*ALPHA + 15*BETA + 3*ALPHA^2 + 3*ALPHA*BETA + 3*BETA*ALPHA + 3*BETA^2
> 9 + 4*BETA + 4*ALPHA + 3*ALPHA^2 + 3*BETA^2
= [plus(times(BETA, dx(ALPHA)), times(ALPHA, dx(BETA)))]
[dx(minus(ALPHA, BETA))] = 8 + 9*ALPHA + 9*BETA + 3*ALPHA^2 + 3*ALPHA*BETA + 3*BETA*ALPHA + 3*BETA^2
> 5 + 3*ALPHA + 3*ALPHA^2 + 3*BETA + 3*BETA^2
= [minus(dx(ALPHA), dx(BETA))]
[dx(neg(ALPHA))] = 20 + 15*ALPHA + 3*ALPHA^2
> 4 + 3*ALPHA + 3*ALPHA^2
= [neg(dx(ALPHA))]
[dx(div(ALPHA, BETA))] = 38 + 21*ALPHA + 21*BETA + 3*ALPHA^2 + 3*ALPHA*BETA + 3*BETA*ALPHA + 3*BETA^2
> 17 + 4*ALPHA + 3*ALPHA^2 + 5*BETA + 3*BETA^2
= [minus(div(dx(ALPHA), BETA),
times(ALPHA, div(dx(BETA), exp(BETA, two()))))]
[dx(exp(ALPHA, BETA))] = 38 + 21*ALPHA + 21*BETA + 3*ALPHA^2 + 3*ALPHA*BETA + 3*BETA*ALPHA + 3*BETA^2
> 21 + 6*BETA + 6*ALPHA + 3*ALPHA^2 + 3*BETA^2
= [plus(times(BETA,
times(exp(ALPHA, minus(BETA, one())), dx(ALPHA))),
times(exp(ALPHA, BETA), times(ln(ALPHA), dx(BETA))))]
[dx(ln(ALPHA))] = 8 + 9*ALPHA + 3*ALPHA^2
> 5 + 4*ALPHA + 3*ALPHA^2
= [div(dx(ALPHA), ALPHA)]
Hurray, we answered YES(?,O(n^2))
lmpo
YES(?,ELEMENTARY)
We are left with following problem, upon which TcT provides the
certificate YES(?,ELEMENTARY).
Strict Trs:
{ 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)))) }
Obligation:
innermost runtime complexity
Answer:
YES(?,ELEMENTARY)
The input was oriented with the instance of 'Lightweight Multiset
Path Order' as induced by the safe mapping
safe(dx) = {}, safe(one) = {}, safe(a) = {}, safe(zero) = {},
safe(plus) = {1, 2}, safe(times) = {1, 2}, safe(minus) = {1, 2},
safe(neg) = {1}, safe(div) = {1, 2}, safe(exp) = {1, 2},
safe(two) = {}, safe(ln) = {1}
and precedence
empty .
Following symbols are considered recursive:
{dx}
The recursion depth is 1.
For your convenience, here are the oriented rules in predicative
notation, possibly applying argument filtering:
Strict DPs:
Weak DPs :
Strict Trs:
{ 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;)))) }
Weak Trs :
Hurray, we answered YES(?,ELEMENTARY)
mpo
YES(?,PRIMREC)
We are left with following problem, upon which TcT provides the
certificate YES(?,PRIMREC).
Strict Trs:
{ 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)))) }
Obligation:
innermost runtime complexity
Answer:
YES(?,PRIMREC)
The input was oriented with the instance of'multiset path orders'
as induced by the precedence
dx > one, dx > plus, dx > times, dx > minus, dx > neg, dx > div,
dx > exp, dx > two, dx > ln, a ~ zero .
Hurray, we answered YES(?,PRIMREC)
popstar
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ 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)))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ 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)))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..