WORST_CASE(Omega(n^1),O(n^2)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^2)) + Considered Problem: - Strict TRS: D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) D'(constant()) -> c1() D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(minus(z0)) -> c8(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) D'(t()) -> c() - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,constant,div,ln,minus,pow,t} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) D'(constant()) -> c1() D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(minus(z0)) -> c8(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) D'(t()) -> c() - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,constant,div,ln,minus,pow,t} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) D'(constant()) -> c1() D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(minus(z0)) -> c8(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) D'(t()) -> c() - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,constant,div,ln,minus,pow,t} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: D'(x){x -> *(x,y)} = D'(*(x,y)) ->^+ c4(D'(x)) = C[D'(x) = D'(x){}] ** Step 1.b:1: NaturalMI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) D'(constant()) -> c1() D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(minus(z0)) -> c8(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) D'(t()) -> c() - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,constant,div,ln,minus,pow,t} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: 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(c10) = {1}, uargs(c11) = {1}, uargs(c12) = {1}, uargs(c13) = {1}, uargs(c2) = {1}, uargs(c3) = {1}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c6) = {1}, uargs(c7) = {1}, uargs(c8) = {1}, uargs(c9) = {1}, uargs(div) = {1}, uargs(minus) = {1} Following symbols are considered usable: {D,D'} TcT has computed the following interpretation: p(*) = [1] x2 + [0] p(+) = [1] x1 + [1] x2 + [0] p(-) = [1] x1 + [1] x2 + [0] p(0) = [0] p(1) = [0] p(2) = [1] p(D) = [0] p(D') = [1] p(c) = [1] p(c1) = [0] p(c10) = [1] x1 + [0] p(c11) = [1] x1 + [0] p(c12) = [1] x1 + [0] p(c13) = [1] x1 + [0] p(c2) = [1] x1 + [0] p(c3) = [1] x1 + [0] p(c4) = [1] x1 + [0] p(c5) = [1] x1 + [0] p(c6) = [1] x1 + [0] p(c7) = [1] x1 + [0] p(c8) = [1] x1 + [0] p(c9) = [1] x1 + [0] p(constant) = [0] p(div) = [1] x1 + [0] p(ln) = [1] x1 + [0] p(minus) = [1] x1 + [0] p(pow) = [1] x2 + [0] p(t) = [0] Following rules are strictly oriented: D'(constant()) = [1] > [0] = c1() Following rules are (at-least) weakly oriented: D(*(z0,z1)) = [0] >= [0] = +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) = [0] >= [0] = +(D(z0),D(z1)) D(-(z0,z1)) = [0] >= [0] = -(D(z0),D(z1)) D(constant()) = [0] >= [0] = 0() D(div(z0,z1)) = [0] >= [0] = -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) = [0] >= [0] = div(D(z0),z0) D(minus(z0)) = [0] >= [0] = minus(D(z0)) D(pow(z0,z1)) = [0] >= [0] = +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) = [0] >= [0] = 1() D'(*(z0,z1)) = [1] >= [1] = c4(D'(z0)) D'(*(z0,z1)) = [1] >= [1] = c5(D'(z1)) D'(+(z0,z1)) = [1] >= [1] = c2(D'(z0)) D'(+(z0,z1)) = [1] >= [1] = c3(D'(z1)) D'(-(z0,z1)) = [1] >= [1] = c6(D'(z0)) D'(-(z0,z1)) = [1] >= [1] = c7(D'(z1)) D'(div(z0,z1)) = [1] >= [1] = c10(D'(z1)) D'(div(z0,z1)) = [1] >= [1] = c9(D'(z0)) D'(ln(z0)) = [1] >= [1] = c11(D'(z0)) D'(minus(z0)) = [1] >= [1] = c8(D'(z0)) D'(pow(z0,z1)) = [1] >= [1] = c12(D'(z0)) D'(pow(z0,z1)) = [1] >= [1] = c13(D'(z1)) D'(t()) = [1] >= [1] = c() ** Step 1.b:2: NaturalMI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(minus(z0)) -> c8(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) D'(t()) -> c() - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() D'(constant()) -> c1() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,constant,div,ln,minus,pow,t} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: 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(c10) = {1}, uargs(c11) = {1}, uargs(c12) = {1}, uargs(c13) = {1}, uargs(c2) = {1}, uargs(c3) = {1}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c6) = {1}, uargs(c7) = {1}, uargs(c8) = {1}, uargs(c9) = {1}, uargs(div) = {1}, uargs(minus) = {1} Following symbols are considered usable: {D,D'} TcT has computed the following interpretation: p(*) = [1] x2 + [0] p(+) = [1] x1 + [1] x2 + [0] p(-) = [1] x1 + [1] x2 + [0] p(0) = [0] p(1) = [0] p(2) = [3] p(D) = [0] p(D') = [1] p(c) = [0] p(c1) = [0] p(c10) = [1] x1 + [0] p(c11) = [1] x1 + [0] p(c12) = [1] x1 + [0] p(c13) = [1] x1 + [0] p(c2) = [1] x1 + [0] p(c3) = [1] x1 + [0] p(c4) = [1] x1 + [0] p(c5) = [1] x1 + [0] p(c6) = [1] x1 + [0] p(c7) = [1] x1 + [0] p(c8) = [1] x1 + [0] p(c9) = [1] x1 + [0] p(constant) = [4] p(div) = [1] x1 + [0] p(ln) = [1] x1 + [0] p(minus) = [1] x1 + [0] p(pow) = [1] x2 + [0] p(t) = [0] Following rules are strictly oriented: D'(t()) = [1] > [0] = c() Following rules are (at-least) weakly oriented: D(*(z0,z1)) = [0] >= [0] = +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) = [0] >= [0] = +(D(z0),D(z1)) D(-(z0,z1)) = [0] >= [0] = -(D(z0),D(z1)) D(constant()) = [0] >= [0] = 0() D(div(z0,z1)) = [0] >= [0] = -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) = [0] >= [0] = div(D(z0),z0) D(minus(z0)) = [0] >= [0] = minus(D(z0)) D(pow(z0,z1)) = [0] >= [0] = +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) = [0] >= [0] = 1() D'(*(z0,z1)) = [1] >= [1] = c4(D'(z0)) D'(*(z0,z1)) = [1] >= [1] = c5(D'(z1)) D'(+(z0,z1)) = [1] >= [1] = c2(D'(z0)) D'(+(z0,z1)) = [1] >= [1] = c3(D'(z1)) D'(-(z0,z1)) = [1] >= [1] = c6(D'(z0)) D'(-(z0,z1)) = [1] >= [1] = c7(D'(z1)) D'(constant()) = [1] >= [0] = c1() D'(div(z0,z1)) = [1] >= [1] = c10(D'(z1)) D'(div(z0,z1)) = [1] >= [1] = c9(D'(z0)) D'(ln(z0)) = [1] >= [1] = c11(D'(z0)) D'(minus(z0)) = [1] >= [1] = c8(D'(z0)) D'(pow(z0,z1)) = [1] >= [1] = c12(D'(z0)) D'(pow(z0,z1)) = [1] >= [1] = c13(D'(z1)) ** Step 1.b:3: NaturalPI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(minus(z0)) -> c8(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() D'(constant()) -> c1() D'(t()) -> c() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,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(c10) = {1}, uargs(c11) = {1}, uargs(c12) = {1}, uargs(c13) = {1}, uargs(c2) = {1}, uargs(c3) = {1}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c6) = {1}, uargs(c7) = {1}, uargs(c8) = {1}, uargs(c9) = {1}, uargs(div) = {1}, uargs(minus) = {1} Following symbols are considered usable: {D,D'} TcT has computed the following interpretation: p(*) = 2 + x1 + x2 p(+) = x1 + x2 p(-) = x1 + x2 p(0) = 0 p(1) = 0 p(2) = 6 p(D) = 3*x1 + 2*x1^2 p(D') = 1 + 2*x1 p(c) = 0 p(c1) = 3 p(c10) = x1 p(c11) = 1 + x1 p(c12) = x1 p(c13) = 3 + x1 p(c2) = x1 p(c3) = x1 p(c4) = x1 p(c5) = 2 + x1 p(c6) = x1 p(c7) = x1 p(c8) = x1 p(c9) = 1 + x1 p(constant) = 2 p(div) = 2 + x1 + x2 p(ln) = 2 + x1 p(minus) = x1 p(pow) = 2 + x1 + x2 p(t) = 2 Following rules are strictly oriented: D'(*(z0,z1)) = 5 + 2*z0 + 2*z1 > 1 + 2*z0 = c4(D'(z0)) D'(*(z0,z1)) = 5 + 2*z0 + 2*z1 > 3 + 2*z1 = c5(D'(z1)) D'(div(z0,z1)) = 5 + 2*z0 + 2*z1 > 1 + 2*z1 = c10(D'(z1)) D'(div(z0,z1)) = 5 + 2*z0 + 2*z1 > 2 + 2*z0 = c9(D'(z0)) D'(ln(z0)) = 5 + 2*z0 > 2 + 2*z0 = c11(D'(z0)) D'(pow(z0,z1)) = 5 + 2*z0 + 2*z1 > 1 + 2*z0 = c12(D'(z0)) D'(pow(z0,z1)) = 5 + 2*z0 + 2*z1 > 4 + 2*z1 = c13(D'(z1)) Following rules are (at-least) weakly oriented: D(*(z0,z1)) = 14 + 11*z0 + 4*z0*z1 + 2*z0^2 + 11*z1 + 2*z1^2 >= 4 + 4*z0 + 2*z0^2 + 4*z1 + 2*z1^2 = +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) = 3*z0 + 4*z0*z1 + 2*z0^2 + 3*z1 + 2*z1^2 >= 3*z0 + 2*z0^2 + 3*z1 + 2*z1^2 = +(D(z0),D(z1)) D(-(z0,z1)) = 3*z0 + 4*z0*z1 + 2*z0^2 + 3*z1 + 2*z1^2 >= 3*z0 + 2*z0^2 + 3*z1 + 2*z1^2 = -(D(z0),D(z1)) D(constant()) = 14 >= 0 = 0() D(div(z0,z1)) = 14 + 11*z0 + 4*z0*z1 + 2*z0^2 + 11*z1 + 2*z1^2 >= 14 + 4*z0 + 2*z0^2 + 5*z1 + 2*z1^2 = -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) = 14 + 11*z0 + 2*z0^2 >= 2 + 4*z0 + 2*z0^2 = div(D(z0),z0) D(minus(z0)) = 3*z0 + 2*z0^2 >= 3*z0 + 2*z0^2 = minus(D(z0)) D(pow(z0,z1)) = 14 + 11*z0 + 4*z0*z1 + 2*z0^2 + 11*z1 + 2*z1^2 >= 14 + 6*z0 + 2*z0^2 + 6*z1 + 2*z1^2 = +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) = 14 >= 0 = 1() D'(+(z0,z1)) = 1 + 2*z0 + 2*z1 >= 1 + 2*z0 = c2(D'(z0)) D'(+(z0,z1)) = 1 + 2*z0 + 2*z1 >= 1 + 2*z1 = c3(D'(z1)) D'(-(z0,z1)) = 1 + 2*z0 + 2*z1 >= 1 + 2*z0 = c6(D'(z0)) D'(-(z0,z1)) = 1 + 2*z0 + 2*z1 >= 1 + 2*z1 = c7(D'(z1)) D'(constant()) = 5 >= 3 = c1() D'(minus(z0)) = 1 + 2*z0 >= 1 + 2*z0 = c8(D'(z0)) D'(t()) = 5 >= 0 = c() ** Step 1.b:4: NaturalPI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) D'(minus(z0)) -> c8(D'(z0)) - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(constant()) -> c1() D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) D'(t()) -> c() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,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(c10) = {1}, uargs(c11) = {1}, uargs(c12) = {1}, uargs(c13) = {1}, uargs(c2) = {1}, uargs(c3) = {1}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c6) = {1}, uargs(c7) = {1}, uargs(c8) = {1}, uargs(c9) = {1}, uargs(div) = {1}, uargs(minus) = {1} Following symbols are considered usable: {D,D'} TcT has computed the following interpretation: p(*) = 1 + x1 + x2 p(+) = x1 + x2 p(-) = x1 + x2 p(0) = 0 p(1) = 1 p(2) = 0 p(D) = 3*x1 + 2*x1^2 p(D') = 3*x1 + x1^2 p(c) = 0 p(c1) = 0 p(c10) = 2 + x1 p(c11) = x1 p(c12) = x1 p(c13) = x1 p(c2) = x1 p(c3) = x1 p(c4) = 2 + x1 p(c5) = x1 p(c6) = x1 p(c7) = x1 p(c8) = x1 p(c9) = x1 p(constant) = 0 p(div) = 1 + x1 + x2 p(ln) = 2 + x1 p(minus) = 1 + x1 p(pow) = 2 + x1 + x2 p(t) = 2 Following rules are strictly oriented: D'(minus(z0)) = 4 + 5*z0 + z0^2 > 3*z0 + z0^2 = c8(D'(z0)) Following rules are (at-least) weakly oriented: D(*(z0,z1)) = 5 + 7*z0 + 4*z0*z1 + 2*z0^2 + 7*z1 + 2*z1^2 >= 2 + 4*z0 + 2*z0^2 + 4*z1 + 2*z1^2 = +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) = 3*z0 + 4*z0*z1 + 2*z0^2 + 3*z1 + 2*z1^2 >= 3*z0 + 2*z0^2 + 3*z1 + 2*z1^2 = +(D(z0),D(z1)) D(-(z0,z1)) = 3*z0 + 4*z0*z1 + 2*z0^2 + 3*z1 + 2*z1^2 >= 3*z0 + 2*z0^2 + 3*z1 + 2*z1^2 = -(D(z0),D(z1)) D(constant()) = 0 >= 0 = 0() D(div(z0,z1)) = 5 + 7*z0 + 4*z0*z1 + 2*z0^2 + 7*z1 + 2*z1^2 >= 5 + 4*z0 + 2*z0^2 + 5*z1 + 2*z1^2 = -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) = 14 + 11*z0 + 2*z0^2 >= 1 + 4*z0 + 2*z0^2 = div(D(z0),z0) D(minus(z0)) = 5 + 7*z0 + 2*z0^2 >= 1 + 3*z0 + 2*z0^2 = minus(D(z0)) D(pow(z0,z1)) = 14 + 11*z0 + 4*z0*z1 + 2*z0^2 + 11*z1 + 2*z1^2 >= 11 + 6*z0 + 2*z0^2 + 6*z1 + 2*z1^2 = +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) = 14 >= 1 = 1() D'(*(z0,z1)) = 4 + 5*z0 + 2*z0*z1 + z0^2 + 5*z1 + z1^2 >= 2 + 3*z0 + z0^2 = c4(D'(z0)) D'(*(z0,z1)) = 4 + 5*z0 + 2*z0*z1 + z0^2 + 5*z1 + z1^2 >= 3*z1 + z1^2 = c5(D'(z1)) D'(+(z0,z1)) = 3*z0 + 2*z0*z1 + z0^2 + 3*z1 + z1^2 >= 3*z0 + z0^2 = c2(D'(z0)) D'(+(z0,z1)) = 3*z0 + 2*z0*z1 + z0^2 + 3*z1 + z1^2 >= 3*z1 + z1^2 = c3(D'(z1)) D'(-(z0,z1)) = 3*z0 + 2*z0*z1 + z0^2 + 3*z1 + z1^2 >= 3*z0 + z0^2 = c6(D'(z0)) D'(-(z0,z1)) = 3*z0 + 2*z0*z1 + z0^2 + 3*z1 + z1^2 >= 3*z1 + z1^2 = c7(D'(z1)) D'(constant()) = 0 >= 0 = c1() D'(div(z0,z1)) = 4 + 5*z0 + 2*z0*z1 + z0^2 + 5*z1 + z1^2 >= 2 + 3*z1 + z1^2 = c10(D'(z1)) D'(div(z0,z1)) = 4 + 5*z0 + 2*z0*z1 + z0^2 + 5*z1 + z1^2 >= 3*z0 + z0^2 = c9(D'(z0)) D'(ln(z0)) = 10 + 7*z0 + z0^2 >= 3*z0 + z0^2 = c11(D'(z0)) D'(pow(z0,z1)) = 10 + 7*z0 + 2*z0*z1 + z0^2 + 7*z1 + z1^2 >= 3*z0 + z0^2 = c12(D'(z0)) D'(pow(z0,z1)) = 10 + 7*z0 + 2*z0*z1 + z0^2 + 7*z1 + z1^2 >= 3*z1 + z1^2 = c13(D'(z1)) D'(t()) = 10 >= 0 = c() ** Step 1.b:5: NaturalPI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(constant()) -> c1() D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(minus(z0)) -> c8(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) D'(t()) -> c() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,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(c10) = {1}, uargs(c11) = {1}, uargs(c12) = {1}, uargs(c13) = {1}, uargs(c2) = {1}, uargs(c3) = {1}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c6) = {1}, uargs(c7) = {1}, uargs(c8) = {1}, uargs(c9) = {1}, uargs(div) = {1}, uargs(minus) = {1} Following symbols are considered usable: {D,D'} TcT has computed the following interpretation: p(*) = 1 + x1 + x2 p(+) = 2 + x1 + x2 p(-) = x1 + x2 p(0) = 0 p(1) = 0 p(2) = 5 p(D) = 2*x1 + 2*x1^2 p(D') = x1^2 p(c) = 0 p(c1) = 0 p(c10) = 2 + x1 p(c11) = 4 + x1 p(c12) = 1 + x1 p(c13) = 2 + x1 p(c2) = x1 p(c3) = x1 p(c4) = 1 + x1 p(c5) = 1 + x1 p(c6) = x1 p(c7) = x1 p(c8) = x1 p(c9) = x1 p(constant) = 0 p(div) = 2 + x1 + x2 p(ln) = 2 + x1 p(minus) = x1 p(pow) = 2 + x1 + x2 p(t) = 0 Following rules are strictly oriented: D'(+(z0,z1)) = 4 + 4*z0 + 2*z0*z1 + z0^2 + 4*z1 + z1^2 > z0^2 = c2(D'(z0)) D'(+(z0,z1)) = 4 + 4*z0 + 2*z0*z1 + z0^2 + 4*z1 + z1^2 > z1^2 = c3(D'(z1)) Following rules are (at-least) weakly oriented: D(*(z0,z1)) = 4 + 6*z0 + 4*z0*z1 + 2*z0^2 + 6*z1 + 2*z1^2 >= 4 + 3*z0 + 2*z0^2 + 3*z1 + 2*z1^2 = +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) = 12 + 10*z0 + 4*z0*z1 + 2*z0^2 + 10*z1 + 2*z1^2 >= 2 + 2*z0 + 2*z0^2 + 2*z1 + 2*z1^2 = +(D(z0),D(z1)) D(-(z0,z1)) = 2*z0 + 4*z0*z1 + 2*z0^2 + 2*z1 + 2*z1^2 >= 2*z0 + 2*z0^2 + 2*z1 + 2*z1^2 = -(D(z0),D(z1)) D(constant()) = 0 >= 0 = 0() D(div(z0,z1)) = 12 + 10*z0 + 4*z0*z1 + 2*z0^2 + 10*z1 + 2*z1^2 >= 12 + 3*z0 + 2*z0^2 + 4*z1 + 2*z1^2 = -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) = 12 + 10*z0 + 2*z0^2 >= 2 + 3*z0 + 2*z0^2 = div(D(z0),z0) D(minus(z0)) = 2*z0 + 2*z0^2 >= 2*z0 + 2*z0^2 = minus(D(z0)) D(pow(z0,z1)) = 12 + 10*z0 + 4*z0*z1 + 2*z0^2 + 10*z1 + 2*z1^2 >= 12 + 5*z0 + 2*z0^2 + 5*z1 + 2*z1^2 = +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) = 0 >= 0 = 1() D'(*(z0,z1)) = 1 + 2*z0 + 2*z0*z1 + z0^2 + 2*z1 + z1^2 >= 1 + z0^2 = c4(D'(z0)) D'(*(z0,z1)) = 1 + 2*z0 + 2*z0*z1 + z0^2 + 2*z1 + z1^2 >= 1 + z1^2 = c5(D'(z1)) D'(-(z0,z1)) = 2*z0*z1 + z0^2 + z1^2 >= z0^2 = c6(D'(z0)) D'(-(z0,z1)) = 2*z0*z1 + z0^2 + z1^2 >= z1^2 = c7(D'(z1)) D'(constant()) = 0 >= 0 = c1() D'(div(z0,z1)) = 4 + 4*z0 + 2*z0*z1 + z0^2 + 4*z1 + z1^2 >= 2 + z1^2 = c10(D'(z1)) D'(div(z0,z1)) = 4 + 4*z0 + 2*z0*z1 + z0^2 + 4*z1 + z1^2 >= z0^2 = c9(D'(z0)) D'(ln(z0)) = 4 + 4*z0 + z0^2 >= 4 + z0^2 = c11(D'(z0)) D'(minus(z0)) = z0^2 >= z0^2 = c8(D'(z0)) D'(pow(z0,z1)) = 4 + 4*z0 + 2*z0*z1 + z0^2 + 4*z1 + z1^2 >= 1 + z0^2 = c12(D'(z0)) D'(pow(z0,z1)) = 4 + 4*z0 + 2*z0*z1 + z0^2 + 4*z1 + z1^2 >= 2 + z1^2 = c13(D'(z1)) D'(t()) = 0 >= 0 = c() ** Step 1.b:6: NaturalPI. WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(constant()) -> c1() D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(minus(z0)) -> c8(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) D'(t()) -> c() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,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(c10) = {1}, uargs(c11) = {1}, uargs(c12) = {1}, uargs(c13) = {1}, uargs(c2) = {1}, uargs(c3) = {1}, uargs(c4) = {1}, uargs(c5) = {1}, uargs(c6) = {1}, uargs(c7) = {1}, uargs(c8) = {1}, uargs(c9) = {1}, uargs(div) = {1}, uargs(minus) = {1} Following symbols are considered usable: {D,D'} TcT has computed the following interpretation: p(*) = 1 + x1 + x2 p(+) = x1 + x2 p(-) = 2 + x1 + x2 p(0) = 0 p(1) = 1 p(2) = 2 p(D) = 2*x1 + 2*x1^2 p(D') = 4*x1 p(c) = 0 p(c1) = 0 p(c10) = 2 + x1 p(c11) = 1 + x1 p(c12) = 2 + x1 p(c13) = 2 + x1 p(c2) = x1 p(c3) = x1 p(c4) = 1 + x1 p(c5) = x1 p(c6) = x1 p(c7) = x1 p(c8) = 1 + x1 p(c9) = 1 + x1 p(constant) = 0 p(div) = 2 + x1 + x2 p(ln) = 1 + x1 p(minus) = 1 + x1 p(pow) = 2 + x1 + x2 p(t) = 1 Following rules are strictly oriented: D'(-(z0,z1)) = 8 + 4*z0 + 4*z1 > 4*z0 = c6(D'(z0)) D'(-(z0,z1)) = 8 + 4*z0 + 4*z1 > 4*z1 = c7(D'(z1)) Following rules are (at-least) weakly oriented: D(*(z0,z1)) = 4 + 6*z0 + 4*z0*z1 + 2*z0^2 + 6*z1 + 2*z1^2 >= 2 + 3*z0 + 2*z0^2 + 3*z1 + 2*z1^2 = +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) = 2*z0 + 4*z0*z1 + 2*z0^2 + 2*z1 + 2*z1^2 >= 2*z0 + 2*z0^2 + 2*z1 + 2*z1^2 = +(D(z0),D(z1)) D(-(z0,z1)) = 12 + 10*z0 + 4*z0*z1 + 2*z0^2 + 10*z1 + 2*z1^2 >= 2 + 2*z0 + 2*z0^2 + 2*z1 + 2*z1^2 = -(D(z0),D(z1)) D(constant()) = 0 >= 0 = 0() D(div(z0,z1)) = 12 + 10*z0 + 4*z0*z1 + 2*z0^2 + 10*z1 + 2*z1^2 >= 11 + 3*z0 + 2*z0^2 + 4*z1 + 2*z1^2 = -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) = 4 + 6*z0 + 2*z0^2 >= 2 + 3*z0 + 2*z0^2 = div(D(z0),z0) D(minus(z0)) = 4 + 6*z0 + 2*z0^2 >= 1 + 2*z0 + 2*z0^2 = minus(D(z0)) D(pow(z0,z1)) = 12 + 10*z0 + 4*z0*z1 + 2*z0^2 + 10*z1 + 2*z1^2 >= 12 + 5*z0 + 2*z0^2 + 5*z1 + 2*z1^2 = +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) = 4 >= 1 = 1() D'(*(z0,z1)) = 4 + 4*z0 + 4*z1 >= 1 + 4*z0 = c4(D'(z0)) D'(*(z0,z1)) = 4 + 4*z0 + 4*z1 >= 4*z1 = c5(D'(z1)) D'(+(z0,z1)) = 4*z0 + 4*z1 >= 4*z0 = c2(D'(z0)) D'(+(z0,z1)) = 4*z0 + 4*z1 >= 4*z1 = c3(D'(z1)) D'(constant()) = 0 >= 0 = c1() D'(div(z0,z1)) = 8 + 4*z0 + 4*z1 >= 2 + 4*z1 = c10(D'(z1)) D'(div(z0,z1)) = 8 + 4*z0 + 4*z1 >= 1 + 4*z0 = c9(D'(z0)) D'(ln(z0)) = 4 + 4*z0 >= 1 + 4*z0 = c11(D'(z0)) D'(minus(z0)) = 4 + 4*z0 >= 1 + 4*z0 = c8(D'(z0)) D'(pow(z0,z1)) = 8 + 4*z0 + 4*z1 >= 2 + 4*z0 = c12(D'(z0)) D'(pow(z0,z1)) = 8 + 4*z0 + 4*z1 >= 2 + 4*z1 = c13(D'(z1)) D'(t()) = 4 >= 0 = c() ** Step 1.b:7: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: D(*(z0,z1)) -> +(*(z1,D(z0)),*(z0,D(z1))) D(+(z0,z1)) -> +(D(z0),D(z1)) D(-(z0,z1)) -> -(D(z0),D(z1)) D(constant()) -> 0() D(div(z0,z1)) -> -(div(D(z0),z1),div(*(z0,D(z1)),pow(z1,2()))) D(ln(z0)) -> div(D(z0),z0) D(minus(z0)) -> minus(D(z0)) D(pow(z0,z1)) -> +(*(*(z1,pow(z0,-(z1,1()))),D(z0)),*(*(pow(z0,z1),ln(z0)),D(z1))) D(t()) -> 1() D'(*(z0,z1)) -> c4(D'(z0)) D'(*(z0,z1)) -> c5(D'(z1)) D'(+(z0,z1)) -> c2(D'(z0)) D'(+(z0,z1)) -> c3(D'(z1)) D'(-(z0,z1)) -> c6(D'(z0)) D'(-(z0,z1)) -> c7(D'(z1)) D'(constant()) -> c1() D'(div(z0,z1)) -> c10(D'(z1)) D'(div(z0,z1)) -> c9(D'(z0)) D'(ln(z0)) -> c11(D'(z0)) D'(minus(z0)) -> c8(D'(z0)) D'(pow(z0,z1)) -> c12(D'(z0)) D'(pow(z0,z1)) -> c13(D'(z1)) D'(t()) -> c() - Signature: {D/1,D'/1} / {*/2,+/2,-/2,0/0,1/0,2/0,c/0,c1/0,c10/1,c11/1,c12/1,c13/1,c2/1,c3/1,c4/1,c5/1,c6/1,c7/1,c8/1 ,c9/1,constant/0,div/2,ln/1,minus/1,pow/2,t/0} - Obligation: innermost runtime complexity wrt. defined symbols {D,D'} and constructors {*,+,-,0,1,2,c,c1,c10,c11,c12,c13 ,c2,c3,c4,c5,c6,c7,c8,c9,constant,div,ln,minus,pow,t} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^2))