* 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))