```* Step 1: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
D(+(x,y)) -> +(D(x),D(y))
D(-(x,y)) -> -(D(x),D(y))
D(constant()) -> 0()
D(div(x,y)) -> -(div(D(x),y),div(*(x,D(y)),pow(y,2())))
D(ln(x)) -> div(D(x),x)
D(minus(x)) -> minus(D(x))
D(pow(x,y)) -> +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))
D(t()) -> 1()
- Signature:
{D/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0}
- Obligation:
runtime complexity wrt. defined symbols {D} and constructors {*,+,-,0,1,2,constant,div,ln,minus,pow,t}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(*) = {2},
uargs(+) = {1,2},
uargs(-) = {1,2},
uargs(div) = {1},
uargs(minus) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = [1] x2 + [1]
p(+) = [1] x1 + [1] x2 + [4]
p(-) = [1] x1 + [1] x2 + [5]
p(0) = [2]
p(1) = [3]
p(2) = [0]
p(D) = [4]
p(constant) = [1]
p(div) = [1] x1 + [0]
p(ln) = [7]
p(minus) = [1] x1 + [0]
p(pow) = [7]
p(t) = [4]

Following rules are strictly oriented:
D(constant()) = [4]
> [2]
= 0()

D(t()) = [4]
> [3]
= 1()

Following rules are (at-least) weakly oriented:
D(*(x,y)) =  [4]
>= [14]
=  +(*(y,D(x)),*(x,D(y)))

D(+(x,y)) =  [4]
>= [12]
=  +(D(x),D(y))

D(-(x,y)) =  [4]
>= [13]
=  -(D(x),D(y))

D(div(x,y)) =  [4]
>= [14]
=  -(div(D(x),y),div(*(x,D(y)),pow(y,2())))

D(ln(x)) =  [4]
>= [4]
=  div(D(x),x)

D(minus(x)) =  [4]
>= [4]
=  minus(D(x))

D(pow(x,y)) =  [4]
>= [14]
=  +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 2: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
D(+(x,y)) -> +(D(x),D(y))
D(-(x,y)) -> -(D(x),D(y))
D(div(x,y)) -> -(div(D(x),y),div(*(x,D(y)),pow(y,2())))
D(ln(x)) -> div(D(x),x)
D(minus(x)) -> minus(D(x))
D(pow(x,y)) -> +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))
- Weak TRS:
D(constant()) -> 0()
D(t()) -> 1()
- Signature:
{D/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0}
- Obligation:
runtime complexity wrt. defined symbols {D} and constructors {*,+,-,0,1,2,constant,div,ln,minus,pow,t}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(*) = {2},
uargs(+) = {1,2},
uargs(-) = {1,2},
uargs(div) = {1},
uargs(minus) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = 1 + x1 + x2
p(+) = x1 + x2
p(-) = x1 + x2
p(0) = 0
p(1) = 0
p(2) = 0
p(D) = 4*x1 + 4*x1^2
p(constant) = 0
p(div) = 1 + x1 + x2
p(ln) = 1 + x1
p(minus) = x1
p(pow) = 1 + x1 + x2
p(t) = 0

Following rules are strictly oriented:
D(*(x,y)) = 8 + 12*x + 8*x*y + 4*x^2 + 12*y + 4*y^2
> 2 + 5*x + 4*x^2 + 5*y + 4*y^2
= +(*(y,D(x)),*(x,D(y)))

D(div(x,y)) = 8 + 12*x + 8*x*y + 4*x^2 + 12*y + 4*y^2
> 4 + 5*x + 4*x^2 + 6*y + 4*y^2
= -(div(D(x),y),div(*(x,D(y)),pow(y,2())))

D(ln(x)) = 8 + 12*x + 4*x^2
> 1 + 5*x + 4*x^2
= div(D(x),x)

D(pow(x,y)) = 8 + 12*x + 8*x*y + 4*x^2 + 12*y + 4*y^2
> 7 + 7*x + 4*x^2 + 7*y + 4*y^2
= +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))

Following rules are (at-least) weakly oriented:
D(+(x,y)) =  4*x + 8*x*y + 4*x^2 + 4*y + 4*y^2
>= 4*x + 4*x^2 + 4*y + 4*y^2
=  +(D(x),D(y))

D(-(x,y)) =  4*x + 8*x*y + 4*x^2 + 4*y + 4*y^2
>= 4*x + 4*x^2 + 4*y + 4*y^2
=  -(D(x),D(y))

D(constant()) =  0
>= 0
=  0()

D(minus(x)) =  4*x + 4*x^2
>= 4*x + 4*x^2
=  minus(D(x))

D(t()) =  0
>= 0
=  1()

* Step 3: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
D(+(x,y)) -> +(D(x),D(y))
D(-(x,y)) -> -(D(x),D(y))
D(minus(x)) -> minus(D(x))
- Weak TRS:
D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
D(constant()) -> 0()
D(div(x,y)) -> -(div(D(x),y),div(*(x,D(y)),pow(y,2())))
D(ln(x)) -> div(D(x),x)
D(pow(x,y)) -> +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))
D(t()) -> 1()
- Signature:
{D/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0}
- Obligation:
runtime complexity wrt. defined symbols {D} and constructors {*,+,-,0,1,2,constant,div,ln,minus,pow,t}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(*) = {2},
uargs(+) = {1,2},
uargs(-) = {1,2},
uargs(div) = {1},
uargs(minus) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = 1 + x1 + x2
p(+) = x1 + x2
p(-) = x1 + x2
p(0) = 0
p(1) = 0
p(2) = 1
p(D) = x1 + 6*x1^2
p(constant) = 0
p(div) = 1 + x1 + x2
p(ln) = 1 + x1
p(minus) = 1 + x1
p(pow) = 1 + x1 + x2
p(t) = 0

Following rules are strictly oriented:
D(minus(x)) = 7 + 13*x + 6*x^2
> 1 + x + 6*x^2
= minus(D(x))

Following rules are (at-least) weakly oriented:
D(*(x,y)) =  7 + 13*x + 12*x*y + 6*x^2 + 13*y + 6*y^2
>= 2 + 2*x + 6*x^2 + 2*y + 6*y^2
=  +(*(y,D(x)),*(x,D(y)))

D(+(x,y)) =  x + 12*x*y + 6*x^2 + y + 6*y^2
>= x + 6*x^2 + y + 6*y^2
=  +(D(x),D(y))

D(-(x,y)) =  x + 12*x*y + 6*x^2 + y + 6*y^2
>= x + 6*x^2 + y + 6*y^2
=  -(D(x),D(y))

D(constant()) =  0
>= 0
=  0()

D(div(x,y)) =  7 + 13*x + 12*x*y + 6*x^2 + 13*y + 6*y^2
>= 5 + 2*x + 6*x^2 + 3*y + 6*y^2
=  -(div(D(x),y),div(*(x,D(y)),pow(y,2())))

D(ln(x)) =  7 + 13*x + 6*x^2
>= 1 + 2*x + 6*x^2
=  div(D(x),x)

D(pow(x,y)) =  7 + 13*x + 12*x*y + 6*x^2 + 13*y + 6*y^2
>= 7 + 4*x + 6*x^2 + 4*y + 6*y^2
=  +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))

D(t()) =  0
>= 0
=  1()

* Step 4: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
D(+(x,y)) -> +(D(x),D(y))
D(-(x,y)) -> -(D(x),D(y))
- Weak TRS:
D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
D(constant()) -> 0()
D(div(x,y)) -> -(div(D(x),y),div(*(x,D(y)),pow(y,2())))
D(ln(x)) -> div(D(x),x)
D(minus(x)) -> minus(D(x))
D(pow(x,y)) -> +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))
D(t()) -> 1()
- Signature:
{D/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0}
- Obligation:
runtime complexity wrt. defined symbols {D} and constructors {*,+,-,0,1,2,constant,div,ln,minus,pow,t}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(*) = {2},
uargs(+) = {1,2},
uargs(-) = {1,2},
uargs(div) = {1},
uargs(minus) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = 1 + x1 + x2
p(+) = x1 + x2
p(-) = 1 + x1 + x2
p(0) = 0
p(1) = 1
p(2) = 1
p(D) = 4*x1 + 5*x1^2
p(constant) = 0
p(div) = 1 + x1 + x2
p(ln) = 1 + x1
p(minus) = x1
p(pow) = 1 + x1 + x2
p(t) = 1

Following rules are strictly oriented:
D(-(x,y)) = 9 + 14*x + 10*x*y + 5*x^2 + 14*y + 5*y^2
> 1 + 4*x + 5*x^2 + 4*y + 5*y^2
= -(D(x),D(y))

Following rules are (at-least) weakly oriented:
D(*(x,y)) =  9 + 14*x + 10*x*y + 5*x^2 + 14*y + 5*y^2
>= 2 + 5*x + 5*x^2 + 5*y + 5*y^2
=  +(*(y,D(x)),*(x,D(y)))

D(+(x,y)) =  4*x + 10*x*y + 5*x^2 + 4*y + 5*y^2
>= 4*x + 5*x^2 + 4*y + 5*y^2
=  +(D(x),D(y))

D(constant()) =  0
>= 0
=  0()

D(div(x,y)) =  9 + 14*x + 10*x*y + 5*x^2 + 14*y + 5*y^2
>= 6 + 5*x + 5*x^2 + 6*y + 5*y^2
=  -(div(D(x),y),div(*(x,D(y)),pow(y,2())))

D(ln(x)) =  9 + 14*x + 5*x^2
>= 1 + 5*x + 5*x^2
=  div(D(x),x)

D(minus(x)) =  4*x + 5*x^2
>= 4*x + 5*x^2
=  minus(D(x))

D(pow(x,y)) =  9 + 14*x + 10*x*y + 5*x^2 + 14*y + 5*y^2
>= 9 + 7*x + 5*x^2 + 7*y + 5*y^2
=  +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))

D(t()) =  9
>= 1
=  1()

* Step 5: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
D(+(x,y)) -> +(D(x),D(y))
- Weak TRS:
D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
D(-(x,y)) -> -(D(x),D(y))
D(constant()) -> 0()
D(div(x,y)) -> -(div(D(x),y),div(*(x,D(y)),pow(y,2())))
D(ln(x)) -> div(D(x),x)
D(minus(x)) -> minus(D(x))
D(pow(x,y)) -> +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))
D(t()) -> 1()
- Signature:
{D/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0}
- Obligation:
runtime complexity wrt. defined symbols {D} and constructors {*,+,-,0,1,2,constant,div,ln,minus,pow,t}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(*) = {2},
uargs(+) = {1,2},
uargs(-) = {1,2},
uargs(div) = {1},
uargs(minus) = {1}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(*) = 1 + x1 + x2
p(+) = 1 + x1 + x2
p(-) = x1 + x2
p(0) = 1
p(1) = 0
p(2) = 1
p(D) = 7*x1 + 4*x1^2
p(constant) = 1
p(div) = 1 + x1 + x2
p(ln) = 1 + x1
p(minus) = x1
p(pow) = 1 + x1 + x2
p(t) = 1

Following rules are strictly oriented:
D(+(x,y)) = 11 + 15*x + 8*x*y + 4*x^2 + 15*y + 4*y^2
> 1 + 7*x + 4*x^2 + 7*y + 4*y^2
= +(D(x),D(y))

Following rules are (at-least) weakly oriented:
D(*(x,y)) =  11 + 15*x + 8*x*y + 4*x^2 + 15*y + 4*y^2
>= 3 + 8*x + 4*x^2 + 8*y + 4*y^2
=  +(*(y,D(x)),*(x,D(y)))

D(-(x,y)) =  7*x + 8*x*y + 4*x^2 + 7*y + 4*y^2
>= 7*x + 4*x^2 + 7*y + 4*y^2
=  -(D(x),D(y))

D(constant()) =  11
>= 1
=  0()

D(div(x,y)) =  11 + 15*x + 8*x*y + 4*x^2 + 15*y + 4*y^2
>= 5 + 8*x + 4*x^2 + 9*y + 4*y^2
=  -(div(D(x),y),div(*(x,D(y)),pow(y,2())))

D(ln(x)) =  11 + 15*x + 4*x^2
>= 1 + 8*x + 4*x^2
=  div(D(x),x)

D(minus(x)) =  7*x + 4*x^2
>= 7*x + 4*x^2
=  minus(D(x))

D(pow(x,y)) =  11 + 15*x + 8*x*y + 4*x^2 + 15*y + 4*y^2
>= 8 + 10*x + 4*x^2 + 10*y + 4*y^2
=  +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))

D(t()) =  11
>= 0
=  1()

* Step 6: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
D(*(x,y)) -> +(*(y,D(x)),*(x,D(y)))
D(+(x,y)) -> +(D(x),D(y))
D(-(x,y)) -> -(D(x),D(y))
D(constant()) -> 0()
D(div(x,y)) -> -(div(D(x),y),div(*(x,D(y)),pow(y,2())))
D(ln(x)) -> div(D(x),x)
D(minus(x)) -> minus(D(x))
D(pow(x,y)) -> +(*(*(y,pow(x,-(y,1()))),D(x)),*(*(pow(x,y),ln(x)),D(y)))
D(t()) -> 1()
- Signature:
{D/1} / {*/2,+/2,-/2,0/0,1/0,2/0,constant/0,div/2,ln/1,minus/1,pow/2,t/0}
- Obligation:
runtime complexity wrt. defined symbols {D} and constructors {*,+,-,0,1,2,constant,div,ln,minus,pow,t}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))
```