WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum WORST_CASE(Omega(n^1),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: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(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: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: dx(x){x -> div(x,y)} = dx(div(x,y)) ->^+ minus(div(dx(x),y),times(x,div(dx(y),exp(y,two())))) = C[dx(x) = dx(x){}] ** Step 1.b:1: Ara 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: Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = 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)] -(0)-> "A"(0) exp :: ["A"(15) x "A"(15)] -(15)-> "A"(15) exp :: ["A"(0) x "A"(0)] -(0)-> "A"(0) ln :: ["A"(15)] -(0)-> "A"(15) ln :: ["A"(0)] -(0)-> "A"(0) minus :: ["A"(15) x "A"(15)] -(0)-> "A"(15) minus :: ["A"(0) x "A"(0)] -(0)-> "A"(0) neg :: ["A"(15)] -(0)-> "A"(15) neg :: ["A"(0)] -(0)-> "A"(0) one :: [] -(0)-> "A"(14) one :: [] -(0)-> "A"(12) plus :: ["A"(15) x "A"(15)] -(15)-> "A"(15) plus :: ["A"(0) x "A"(0)] -(0)-> "A"(0) times :: ["A"(15) x "A"(15)] -(0)-> "A"(15) times :: ["A"(0) x "A"(0)] -(0)-> "A"(0) two :: [] -(0)-> "A"(14) zero :: [] -(0)-> "A"(10) Cost-free Signatures used: -------------------------- 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)] -(0)-> "A"(1) "minus_A" :: ["A"(1) x "A"(1)] -(0)-> "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)] -(0)-> "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(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(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) ** Step 1.b:2: Ara 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(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) - Weak TRS: 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 {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- a :: [] -(0)-> "A"(12) div :: ["A"(12) x "A"(12)] -(12)-> "A"(12) div :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dx :: ["A"(12)] -(0)-> "A"(0) exp :: ["A"(12) x "A"(12)] -(12)-> "A"(12) exp :: ["A"(0) x "A"(0)] -(0)-> "A"(0) ln :: ["A"(12)] -(12)-> "A"(12) ln :: ["A"(0)] -(0)-> "A"(0) minus :: ["A"(12) x "A"(12)] -(12)-> "A"(12) minus :: ["A"(0) x "A"(0)] -(0)-> "A"(0) neg :: ["A"(12)] -(12)-> "A"(12) neg :: ["A"(0)] -(0)-> "A"(0) one :: [] -(0)-> "A"(8) plus :: ["A"(12) x "A"(12)] -(0)-> "A"(12) plus :: ["A"(0) x "A"(0)] -(0)-> "A"(0) times :: ["A"(12) x "A"(12)] -(12)-> "A"(12) times :: ["A"(0) x "A"(0)] -(0)-> "A"(0) two :: [] -(0)-> "A"(8) zero :: [] -(0)-> "A"(8) Cost-free Signatures used: -------------------------- 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)] -(0)-> "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())))) dx(ln(ALPHA)) -> div(dx(ALPHA),ALPHA) dx(neg(ALPHA)) -> neg(dx(ALPHA)) 2. Weak: dx(X) -> one() dx(a()) -> zero() 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(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) ** Step 1.b:3: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dx(X) -> one() dx(a()) -> zero() 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(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) - Weak TRS: 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(neg(ALPHA)) -> neg(dx(ALPHA)) 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 {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = 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)] -(2)-> "A"(0) exp :: ["A"(14) x "A"(14)] -(14)-> "A"(14) exp :: ["A"(0) x "A"(0)] -(0)-> "A"(0) ln :: ["A"(14)] -(0)-> "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)] -(0)-> "A"(14) neg :: ["A"(0)] -(0)-> "A"(0) one :: [] -(0)-> "A"(8) one :: [] -(0)-> "A"(12) 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"(8) Cost-free Signatures used: -------------------------- 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)] -(0)-> "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(a()) -> zero() 2. Weak: dx(X) -> one() 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(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) ** Step 1.b:4: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dx(X) -> one() 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(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) dx(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) - Weak TRS: 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(neg(ALPHA)) -> neg(dx(ALPHA)) 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 {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = 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)] -(1)-> "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)] -(13)-> "A"(13) neg :: ["A"(0)] -(0)-> "A"(0) one :: [] -(0)-> "A"(8) one :: [] -(0)-> "A"(10) 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"(14) Cost-free Signatures used: -------------------------- 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(times(ALPHA,BETA)) -> plus(times(BETA,dx(ALPHA)),times(ALPHA,dx(BETA))) 2. Weak: dx(X) -> one() 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(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) ** Step 1.b:5: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dx(X) -> one() 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(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) - Weak TRS: 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(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 {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- a :: [] -(0)-> "A"(12) div :: ["A"(12) x "A"(12)] -(12)-> "A"(12) div :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dx :: ["A"(12)] -(0)-> "A"(0) exp :: ["A"(12) x "A"(12)] -(12)-> "A"(12) exp :: ["A"(0) x "A"(0)] -(0)-> "A"(0) ln :: ["A"(12)] -(12)-> "A"(12) ln :: ["A"(0)] -(0)-> "A"(0) minus :: ["A"(12) x "A"(12)] -(12)-> "A"(12) minus :: ["A"(0) x "A"(0)] -(0)-> "A"(0) neg :: ["A"(12)] -(0)-> "A"(12) neg :: ["A"(0)] -(0)-> "A"(0) one :: [] -(0)-> "A"(8) plus :: ["A"(12) x "A"(12)] -(12)-> "A"(12) plus :: ["A"(0) x "A"(0)] -(0)-> "A"(0) times :: ["A"(12) x "A"(12)] -(12)-> "A"(12) times :: ["A"(0) x "A"(0)] -(0)-> "A"(0) two :: [] -(0)-> "A"(12) zero :: [] -(0)-> "A"(8) Cost-free Signatures used: -------------------------- 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(minus(ALPHA,BETA)) -> minus(dx(ALPHA),dx(BETA)) 2. Weak: dx(X) -> one() 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 1.b:6: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dx(X) -> one() 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(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 {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- a :: [] -(0)-> "A"(9) div :: ["A"(9) x "A"(9)] -(9)-> "A"(9) div :: ["A"(0) x "A"(0)] -(0)-> "A"(0) dx :: ["A"(9)] -(1)-> "A"(0) exp :: ["A"(9) x "A"(9)] -(9)-> "A"(9) exp :: ["A"(0) x "A"(0)] -(0)-> "A"(0) ln :: ["A"(9)] -(9)-> "A"(9) ln :: ["A"(0)] -(0)-> "A"(0) minus :: ["A"(9) x "A"(9)] -(9)-> "A"(9) minus :: ["A"(0) x "A"(0)] -(0)-> "A"(0) neg :: ["A"(9)] -(9)-> "A"(9) neg :: ["A"(0)] -(0)-> "A"(0) one :: [] -(0)-> "A"(8) plus :: ["A"(9) x "A"(9)] -(9)-> "A"(9) plus :: ["A"(0) x "A"(0)] -(0)-> "A"(0) times :: ["A"(9) x "A"(9)] -(9)-> "A"(9) times :: ["A"(0) x "A"(0)] -(0)-> "A"(0) two :: [] -(0)-> "A"(8) zero :: [] -(0)-> "A"(8) Cost-free Signatures used: -------------------------- 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(X) -> one() 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: WORST_CASE(Omega(n^1),O(n^1))