WORST_CASE(?,O(n^1))
* Step 1: WeightGap WORST_CASE(?,O(n^1))
+ 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:
innermost 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) = [2]
p(div) = [1] x1 + [0]
p(dx) = [2]
p(exp) = [0]
p(ln) = [1]
p(minus) = [1] x1 + [1] x2 + [2]
p(neg) = [1] x1 + [4]
p(one) = [1]
p(plus) = [1] x1 + [1] x2 + [5]
p(times) = [1] x2 + [1]
p(two) = [1]
p(zero) = [0]
Following rules are strictly oriented:
dx(X) = [2]
> [1]
= one()
dx(a()) = [2]
> [0]
= zero()
Following rules are (at-least) weakly oriented:
dx(div(ALPHA,BETA)) = [2]
>= [7]
= minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
dx(exp(ALPHA,BETA)) = [2]
>= [13]
= plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
dx(ln(ALPHA)) = [2]
>= [2]
= div(dx(ALPHA),ALPHA)
dx(minus(ALPHA,BETA)) = [2]
>= [6]
= minus(dx(ALPHA),dx(BETA))
dx(neg(ALPHA)) = [2]
>= [6]
= neg(dx(ALPHA))
dx(plus(ALPHA,BETA)) = [2]
>= [9]
= plus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) = [2]
>= [11]
= 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: Ara WORST_CASE(?,O(n^1))
+ 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:
innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
,times,two,zero}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
a :: [] -(0)-> A(13)
div :: [A(13) x A(13)] -(13)-> A(13)
div :: [A(0) x A(0)] -(0)-> A(0)
dx :: [A(13)] -(0)-> A(0)
exp :: [A(13) x A(13)] -(13)-> A(13)
exp :: [A(0) x A(0)] -(0)-> A(0)
ln :: [A(13)] -(13)-> A(13)
ln :: [A(0)] -(0)-> A(0)
minus :: [A(13) x A(13)] -(13)-> A(13)
minus :: [A(0) x A(0)] -(0)-> A(0)
neg :: [A(13)] -(0)-> A(13)
neg :: [A(0)] -(0)-> A(0)
one :: [] -(0)-> A(12)
one :: [] -(0)-> A(6)
plus :: [A(13) x A(13)] -(13)-> A(13)
plus :: [A(0) x A(0)] -(0)-> A(0)
times :: [A(13) x A(13)] -(13)-> A(13)
times :: [A(0) x A(0)] -(0)-> A(0)
two :: [] -(0)-> A(12)
zero :: [] -(0)-> A(6)
Cost-free Signatures used:
--------------------------
a :: [] -(0)-> A_cf(0)
div :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
dx :: [A_cf(0)] -(0)-> A_cf(0)
exp :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
ln :: [A_cf(0)] -(0)-> A_cf(0)
minus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
neg :: [A_cf(0)] -(0)-> A_cf(0)
one :: [] -(0)-> A_cf(0)
plus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
times :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
two :: [] -(0)-> A_cf(0)
zero :: [] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
a_A :: [] -(0)-> A(1)
div_A :: [A(1) x A(1)] -(1)-> A(1)
exp_A :: [A(1) x A(1)] -(1)-> A(1)
ln_A :: [A(1)] -(1)-> A(1)
minus_A :: [A(1) x A(1)] -(1)-> A(1)
neg_A :: [A(1)] -(0)-> A(1)
one_A :: [] -(0)-> A(1)
plus_A :: [A(1) x A(1)] -(1)-> A(1)
times_A :: [A(1) x A(1)] -(1)-> A(1)
two_A :: [] -(0)-> A(1)
zero_A :: [] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
dx(plus(ALPHA,BETA)) -> plus(dx(ALPHA),dx(BETA))
2. Weak:
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(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
* Step 3: Ara WORST_CASE(?,O(n^1))
+ 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(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
- Weak TRS:
dx(X) -> one()
dx(a()) -> zero()
dx(plus(ALPHA,BETA)) -> plus(dx(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:
innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
,times,two,zero}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
a :: [] -(0)-> A(15)
div :: [A(15) x A(15)] -(15)-> A(15)
div :: [A(0) x A(0)] -(0)-> A(0)
dx :: [A(15)] -(3)-> A(0)
exp :: [A(15) x A(15)] -(15)-> A(15)
exp :: [A(0) x A(0)] -(0)-> A(0)
ln :: [A(15)] -(15)-> A(15)
ln :: [A(0)] -(0)-> A(0)
minus :: [A(15) x A(15)] -(15)-> A(15)
minus :: [A(0) x A(0)] -(0)-> A(0)
neg :: [A(15)] -(15)-> A(15)
neg :: [A(0)] -(0)-> A(0)
one :: [] -(0)-> A(12)
one :: [] -(0)-> A(6)
plus :: [A(15) x A(15)] -(15)-> A(15)
plus :: [A(0) x A(0)] -(0)-> A(0)
times :: [A(15) x A(15)] -(15)-> A(15)
times :: [A(0) x A(0)] -(0)-> A(0)
two :: [] -(0)-> A(12)
zero :: [] -(0)-> A(6)
Cost-free Signatures used:
--------------------------
a :: [] -(0)-> A_cf(0)
div :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
dx :: [A_cf(0)] -(0)-> A_cf(0)
exp :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
ln :: [A_cf(0)] -(0)-> A_cf(0)
minus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
neg :: [A_cf(0)] -(0)-> A_cf(0)
one :: [] -(0)-> A_cf(0)
plus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
times :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
two :: [] -(0)-> A_cf(0)
zero :: [] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
a_A :: [] -(0)-> A(1)
div_A :: [A(1) x A(1)] -(1)-> A(1)
exp_A :: [A(1) x A(1)] -(1)-> A(1)
ln_A :: [A(1)] -(1)-> A(1)
minus_A :: [A(1) x A(1)] -(1)-> A(1)
neg_A :: [A(1)] -(1)-> A(1)
one_A :: [] -(0)-> A(1)
plus_A :: [A(1) x A(1)] -(1)-> A(1)
times_A :: [A(1) x A(1)] -(1)-> A(1)
two_A :: [] -(0)-> A(1)
zero_A :: [] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA)))
2. Weak:
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(neg(ALPHA)) -> neg(dx(ALPHA))
* Step 4: Ara WORST_CASE(?,O(n^1))
+ 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(neg(ALPHA)) -> neg(dx(ALPHA))
- Weak TRS:
dx(X) -> one()
dx(a()) -> zero()
dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA)
dx(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA))
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:
innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
,times,two,zero}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
a :: [] -(0)-> A(15)
div :: [A(15) x A(15)] -(15)-> A(15)
div :: [A(0) x A(0)] -(0)-> A(0)
dx :: [A(15)] -(4)-> A(0)
exp :: [A(15) x A(15)] -(15)-> A(15)
exp :: [A(0) x A(0)] -(0)-> A(0)
ln :: [A(15)] -(15)-> A(15)
ln :: [A(0)] -(0)-> A(0)
minus :: [A(15) x A(15)] -(15)-> A(15)
minus :: [A(0) x A(0)] -(0)-> A(0)
neg :: [A(15)] -(15)-> A(15)
neg :: [A(0)] -(0)-> A(0)
one :: [] -(0)-> A(12)
one :: [] -(0)-> A(6)
plus :: [A(15) x A(15)] -(15)-> A(15)
plus :: [A(0) x A(0)] -(0)-> A(0)
times :: [A(15) x A(15)] -(15)-> A(15)
times :: [A(0) x A(0)] -(0)-> A(0)
two :: [] -(0)-> A(12)
zero :: [] -(0)-> A(6)
Cost-free Signatures used:
--------------------------
a :: [] -(0)-> A_cf(0)
div :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
dx :: [A_cf(0)] -(0)-> A_cf(0)
exp :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
ln :: [A_cf(0)] -(0)-> A_cf(0)
minus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
neg :: [A_cf(0)] -(0)-> A_cf(0)
one :: [] -(0)-> A_cf(0)
plus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
times :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
two :: [] -(0)-> A_cf(0)
zero :: [] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
a_A :: [] -(0)-> A(1)
div_A :: [A(1) x A(1)] -(1)-> A(1)
exp_A :: [A(1) x A(1)] -(1)-> A(1)
ln_A :: [A(1)] -(1)-> A(1)
minus_A :: [A(1) x A(1)] -(1)-> A(1)
neg_A :: [A(1)] -(1)-> A(1)
one_A :: [] -(0)-> A(1)
plus_A :: [A(1) x A(1)] -(1)-> A(1)
times_A :: [A(1) x A(1)] -(1)-> A(1)
two_A :: [] -(0)-> A(1)
zero_A :: [] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
dx(neg(ALPHA)) -> neg(dx(ALPHA))
2. Weak:
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))))
* Step 5: Ara WORST_CASE(?,O(n^1))
+ 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))))
- Weak TRS:
dx(X) -> one()
dx(a()) -> zero()
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:
innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
,times,two,zero}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
a :: [] -(0)-> A(14)
div :: [A(14) x A(14)] -(14)-> A(14)
div :: [A(0) x A(0)] -(0)-> A(0)
dx :: [A(14)] -(0)-> A(0)
exp :: [A(14) x A(14)] -(14)-> A(14)
exp :: [A(0) x A(0)] -(0)-> A(0)
ln :: [A(14)] -(14)-> A(14)
ln :: [A(0)] -(0)-> A(0)
minus :: [A(14) x A(14)] -(14)-> A(14)
minus :: [A(0) x A(0)] -(0)-> A(0)
neg :: [A(14)] -(14)-> A(14)
neg :: [A(0)] -(0)-> A(0)
one :: [] -(0)-> A(12)
one :: [] -(0)-> A(6)
plus :: [A(14) x A(14)] -(14)-> A(14)
plus :: [A(0) x A(0)] -(0)-> A(0)
times :: [A(14) x A(14)] -(14)-> A(14)
times :: [A(0) x A(0)] -(0)-> A(0)
two :: [] -(0)-> A(12)
zero :: [] -(0)-> A(6)
Cost-free Signatures used:
--------------------------
a :: [] -(0)-> A_cf(0)
div :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
dx :: [A_cf(0)] -(0)-> A_cf(0)
exp :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
ln :: [A_cf(0)] -(0)-> A_cf(0)
minus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
neg :: [A_cf(0)] -(0)-> A_cf(0)
one :: [] -(0)-> A_cf(0)
plus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
times :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
two :: [] -(0)-> A_cf(0)
zero :: [] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
a_A :: [] -(0)-> A(1)
div_A :: [A(1) x A(1)] -(1)-> A(1)
exp_A :: [A(1) x A(1)] -(1)-> A(1)
ln_A :: [A(1)] -(1)-> A(1)
minus_A :: [A(1) x A(1)] -(1)-> A(1)
neg_A :: [A(1)] -(1)-> A(1)
one_A :: [] -(0)-> A(1)
plus_A :: [A(1) x A(1)] -(1)-> A(1)
times_A :: [A(1) x A(1)] -(1)-> A(1)
two_A :: [] -(0)-> A(1)
zero_A :: [] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
dx(div(ALPHA,BETA)) -> minus(div(dx(ALPHA),BETA),times(ALPHA,div(dx(BETA),exp(BETA,two()))))
2. Weak:
dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
* Step 6: Ara WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
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:
dx(X) -> one()
dx(a()) -> zero()
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(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:
innermost runtime complexity wrt. defined symbols {dx} and constructors {a,div,exp,ln,minus,neg,one,plus
,times,two,zero}
+ Applied Processor:
Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 15, araFindStrictRules = Just 1}
+ Details:
Signatures used:
----------------
a :: [] -(0)-> A(14)
div :: [A(14) x A(14)] -(14)-> A(14)
div :: [A(0) x A(0)] -(0)-> A(0)
dx :: [A(14)] -(0)-> A(0)
exp :: [A(14) x A(14)] -(14)-> A(14)
exp :: [A(0) x A(0)] -(0)-> A(0)
ln :: [A(14)] -(14)-> A(14)
ln :: [A(0)] -(0)-> A(0)
minus :: [A(14) x A(14)] -(14)-> A(14)
minus :: [A(0) x A(0)] -(0)-> A(0)
neg :: [A(14)] -(14)-> A(14)
neg :: [A(0)] -(0)-> A(0)
one :: [] -(0)-> A(12)
one :: [] -(0)-> A(6)
plus :: [A(14) x A(14)] -(14)-> A(14)
plus :: [A(0) x A(0)] -(0)-> A(0)
times :: [A(14) x A(14)] -(14)-> A(14)
times :: [A(0) x A(0)] -(0)-> A(0)
two :: [] -(0)-> A(12)
zero :: [] -(0)-> A(6)
Cost-free Signatures used:
--------------------------
a :: [] -(0)-> A_cf(0)
div :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
dx :: [A_cf(0)] -(0)-> A_cf(0)
exp :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
ln :: [A_cf(0)] -(0)-> A_cf(0)
minus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
neg :: [A_cf(0)] -(0)-> A_cf(0)
one :: [] -(0)-> A_cf(0)
plus :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
times :: [A_cf(0) x A_cf(0)] -(0)-> A_cf(0)
two :: [] -(0)-> A_cf(0)
zero :: [] -(0)-> A_cf(0)
Base Constructor Signatures used:
---------------------------------
a_A :: [] -(0)-> A(1)
div_A :: [A(1) x A(1)] -(1)-> A(1)
exp_A :: [A(1) x A(1)] -(1)-> A(1)
ln_A :: [A(1)] -(1)-> A(1)
minus_A :: [A(1) x A(1)] -(1)-> A(1)
neg_A :: [A(1)] -(1)-> A(1)
one_A :: [] -(0)-> A(1)
plus_A :: [A(1) x A(1)] -(1)-> A(1)
times_A :: [A(1) x A(1)] -(1)-> A(1)
two_A :: [] -(0)-> A(1)
zero_A :: [] -(0)-> A(1)
Following Still Strict Rules were Typed as:
-------------------------------------------
1. Strict:
dx(exp(ALPHA,BETA)) -> plus(times(BETA,times(exp(ALPHA,minus(BETA,one())),dx(ALPHA)))
,times(exp(ALPHA,BETA),times(ln(ALPHA),dx(BETA))))
2. Weak:
* Step 7: 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:
innermost 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^1))