* Step 1: WeightGap WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
dx(X) -> one()
dx(a()) -> zero()
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)
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) -> neg(dx(ALPHA))
dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
- Signature:
{dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
- Obligation:
runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus,times,two
,zero}
+ 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(div) = {1},
uargs(minus) = {1,2},
uargs(neg) = {1},
uargs(plus) = {1,2},
uargs(times) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(a) = [0]
p(div) = [1] x1 + [0]
p(dx) = [1]
p(exp) = [1] x2 + [2]
p(ln) = [2]
p(minus) = [1] x1 + [1] x2 + [1]
p(neg) = [1] x1 + [0]
p(one) = [0]
p(plus) = [1] x1 + [1] x2 + [5]
p(times) = [1] x2 + [0]
p(two) = [1]
p(zero) = [0]
Following rules are strictly oriented:
dx(X) = [1]
> [0]
= one()
dx(a()) = [1]
> [0]
= zero()
Following rules are (at-least) weakly oriented:
dx(div(ALPHA,BETA)) = [1]
>= [3]
= minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
dx(exp(ALPHA,BETA)) = [1]
>= [7]
= plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
dx(ln(ALPHA)) = [1]
>= [1]
= div(dx(ALPHA),ALPHA)
dx(minus(ALPHA,BETA)) = [1]
>= [3]
= minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) = [1]
>= [1]
= neg(dx(ALPHA))
dx(plus(ALPHA,BETA)) = [1]
>= [7]
= plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) = [1]
>= [7]
= plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
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:
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)
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) -> neg(dx(ALPHA))
dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
- Weak TRS:
dx(X) -> one()
dx(a()) -> zero()
- Signature:
{dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
- Obligation:
runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus,times,two
,zero}
+ 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(div) = {1},
uargs(minus) = {1,2},
uargs(neg) = {1},
uargs(plus) = {1,2},
uargs(times) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(a) = 0
p(div) = 1 + x1 + x2
p(dx) = 4*x1 + 4*x1^2
p(exp) = 1 + x1 + x2
p(ln) = 1 + x1
p(minus) = x1 + x2
p(neg) = x1
p(one) = 0
p(plus) = x1 + x2
p(times) = 1 + x1 + x2
p(two) = 1
p(zero) = 0
Following rules are strictly oriented:
dx(div(ALPHA,BETA)) = 8 + 12*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 12*BETA + 4*BETA^2
> 5 + 5*ALPHA + 4*ALPHA^2 + 6*BETA + 4*BETA^2
= minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
dx(exp(ALPHA,BETA)) = 8 + 12*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 12*BETA + 4*BETA^2
> 7 + 7*ALPHA + 4*ALPHA^2 + 7*BETA + 4*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 + 12*ALPHA + 4*ALPHA^2
> 1 + 5*ALPHA + 4*ALPHA^2
= div(dx(ALPHA),ALPHA)
dx(times(ALPHA,BETA)) = 8 + 12*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 12*BETA + 4*BETA^2
> 2 + 5*ALPHA + 4*ALPHA^2 + 5*BETA + 4*BETA^2
= plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
Following rules are (at-least) weakly oriented:
dx(X) = 4*X + 4*X^2
>= 0
= one()
dx(a()) = 0
>= 0
= zero()
dx(minus(ALPHA,BETA)) = 4*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 4*BETA + 4*BETA^2
>= 4*ALPHA + 4*ALPHA^2 + 4*BETA + 4*BETA^2
= minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) = 4*ALPHA + 4*ALPHA^2
>= 4*ALPHA + 4*ALPHA^2
= neg(dx(ALPHA))
dx(plus(ALPHA,BETA)) = 4*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 4*BETA + 4*BETA^2
>= 4*ALPHA + 4*ALPHA^2 + 4*BETA + 4*BETA^2
= plus(dx(ALPHA),dx(BETA))
* Step 3: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) -> neg(dx(ALPHA))
dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
- Weak TRS:
dx(X) -> one()
dx(a()) -> zero()
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)
dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
- Signature:
{dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
- Obligation:
runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus,times,two
,zero}
+ 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(div) = {1},
uargs(minus) = {1,2},
uargs(neg) = {1},
uargs(plus) = {1,2},
uargs(times) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(a) = 0
p(div) = 1 + x1 + x2
p(dx) = 4*x1 + 3*x1^2
p(exp) = 1 + x1 + x2
p(ln) = 1 + x1
p(minus) = x1 + x2
p(neg) = 1 + x1
p(one) = 0
p(plus) = x1 + x2
p(times) = 1 + x1 + x2
p(two) = 1
p(zero) = 0
Following rules are strictly oriented:
dx(neg(ALPHA)) = 7 + 10*ALPHA + 3*ALPHA^2
> 1 + 4*ALPHA + 3*ALPHA^2
= neg(dx(ALPHA))
Following rules are (at-least) weakly oriented:
dx(X) = 4*X + 3*X^2
>= 0
= one()
dx(a()) = 0
>= 0
= zero()
dx(div(ALPHA,BETA)) = 7 + 10*ALPHA + 6*ALPHA*BETA + 3*ALPHA^2 + 10*BETA + 3*BETA^2
>= 5 + 5*ALPHA + 3*ALPHA^2 + 6*BETA + 3*BETA^2
= minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
dx(exp(ALPHA,BETA)) = 7 + 10*ALPHA + 6*ALPHA*BETA + 3*ALPHA^2 + 10*BETA + 3*BETA^2
>= 7 + 7*ALPHA + 3*ALPHA^2 + 7*BETA + 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)) = 7 + 10*ALPHA + 3*ALPHA^2
>= 1 + 5*ALPHA + 3*ALPHA^2
= div(dx(ALPHA),ALPHA)
dx(minus(ALPHA,BETA)) = 4*ALPHA + 6*ALPHA*BETA + 3*ALPHA^2 + 4*BETA + 3*BETA^2
>= 4*ALPHA + 3*ALPHA^2 + 4*BETA + 3*BETA^2
= minus(dx(ALPHA),dx(BETA))
dx(plus(ALPHA,BETA)) = 4*ALPHA + 6*ALPHA*BETA + 3*ALPHA^2 + 4*BETA + 3*BETA^2
>= 4*ALPHA + 3*ALPHA^2 + 4*BETA + 3*BETA^2
= plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) = 7 + 10*ALPHA + 6*ALPHA*BETA + 3*ALPHA^2 + 10*BETA + 3*BETA^2
>= 2 + 5*ALPHA + 3*ALPHA^2 + 5*BETA + 3*BETA^2
= plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
* Step 4: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
- Weak TRS:
dx(X) -> one()
dx(a()) -> zero()
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)
dx(neg(ALPHA)) -> neg(dx(ALPHA))
dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
- Signature:
{dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
- Obligation:
runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus,times,two
,zero}
+ 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(div) = {1},
uargs(minus) = {1,2},
uargs(neg) = {1},
uargs(plus) = {1,2},
uargs(times) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(a) = 0
p(div) = 1 + x1 + x2
p(dx) = 5*x1 + 4*x1^2
p(exp) = 1 + x1 + x2
p(ln) = 1 + x1
p(minus) = x1 + x2
p(neg) = x1
p(one) = 0
p(plus) = 1 + x1 + x2
p(times) = 1 + x1 + x2
p(two) = 1
p(zero) = 0
Following rules are strictly oriented:
dx(plus(ALPHA,BETA)) = 9 + 13*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 13*BETA + 4*BETA^2
> 1 + 5*ALPHA + 4*ALPHA^2 + 5*BETA + 4*BETA^2
= plus(dx(ALPHA),dx(BETA))
Following rules are (at-least) weakly oriented:
dx(X) = 5*X + 4*X^2
>= 0
= one()
dx(a()) = 0
>= 0
= zero()
dx(div(ALPHA,BETA)) = 9 + 13*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 13*BETA + 4*BETA^2
>= 5 + 6*ALPHA + 4*ALPHA^2 + 7*BETA + 4*BETA^2
= minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
dx(exp(ALPHA,BETA)) = 9 + 13*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 13*BETA + 4*BETA^2
>= 8 + 8*ALPHA + 4*ALPHA^2 + 8*BETA + 4*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)) = 9 + 13*ALPHA + 4*ALPHA^2
>= 1 + 6*ALPHA + 4*ALPHA^2
= div(dx(ALPHA),ALPHA)
dx(minus(ALPHA,BETA)) = 5*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 5*BETA + 4*BETA^2
>= 5*ALPHA + 4*ALPHA^2 + 5*BETA + 4*BETA^2
= minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) = 5*ALPHA + 4*ALPHA^2
>= 5*ALPHA + 4*ALPHA^2
= neg(dx(ALPHA))
dx(times(ALPHA,BETA)) = 9 + 13*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 13*BETA + 4*BETA^2
>= 3 + 6*ALPHA + 4*ALPHA^2 + 6*BETA + 4*BETA^2
= plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
* Step 5: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
- Weak TRS:
dx(X) -> one()
dx(a()) -> zero()
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)
dx(neg(ALPHA)) -> neg(dx(ALPHA))
dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
- Signature:
{dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
- Obligation:
runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus,times,two
,zero}
+ 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(div) = {1},
uargs(minus) = {1,2},
uargs(neg) = {1},
uargs(plus) = {1,2},
uargs(times) = {2}
Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(a) = 0
p(div) = 1 + x1 + x2
p(dx) = 4*x1 + 4*x1^2
p(exp) = 1 + x1 + x2
p(ln) = 1 + x1
p(minus) = 1 + x1 + x2
p(neg) = x1
p(one) = 0
p(plus) = x1 + x2
p(times) = 1 + x1 + x2
p(two) = 1
p(zero) = 0
Following rules are strictly oriented:
dx(minus(ALPHA,BETA)) = 8 + 12*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 12*BETA + 4*BETA^2
> 1 + 4*ALPHA + 4*ALPHA^2 + 4*BETA + 4*BETA^2
= minus(dx(ALPHA),dx(BETA))
Following rules are (at-least) weakly oriented:
dx(X) = 4*X + 4*X^2
>= 0
= one()
dx(a()) = 0
>= 0
= zero()
dx(div(ALPHA,BETA)) = 8 + 12*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 12*BETA + 4*BETA^2
>= 6 + 5*ALPHA + 4*ALPHA^2 + 6*BETA + 4*BETA^2
= minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
dx(exp(ALPHA,BETA)) = 8 + 12*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 12*BETA + 4*BETA^2
>= 8 + 7*ALPHA + 4*ALPHA^2 + 7*BETA + 4*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 + 12*ALPHA + 4*ALPHA^2
>= 1 + 5*ALPHA + 4*ALPHA^2
= div(dx(ALPHA),ALPHA)
dx(neg(ALPHA)) = 4*ALPHA + 4*ALPHA^2
>= 4*ALPHA + 4*ALPHA^2
= neg(dx(ALPHA))
dx(plus(ALPHA,BETA)) = 4*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 4*BETA + 4*BETA^2
>= 4*ALPHA + 4*ALPHA^2 + 4*BETA + 4*BETA^2
= plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) = 8 + 12*ALPHA + 8*ALPHA*BETA + 4*ALPHA^2 + 12*BETA + 4*BETA^2
>= 2 + 5*ALPHA + 4*ALPHA^2 + 5*BETA + 4*BETA^2
= plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
* Step 6: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
dx(X) -> one()
dx(a()) -> zero()
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)
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) -> neg(dx(ALPHA))
dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
- Signature:
{dx/1} / {a/0,div/2,exp/2,ln/1,minus/2,neg/1,one/0,plus/2,times/2,two/0,zero/0}
- Obligation:
runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus,times,two
,zero}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))