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