WORST_CASE(?,O(n^2)) * Step 1: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: *(0(),y) -> 0() *(s(x),y) -> +(y,*(x,y)) -(x,0()) -> x -(0(),y) -> 0() -(s(x),s(y)) -> -(x,y) exp(x,0()) -> s(0()) exp(x,s(y)) -> *(x,exp(x,y)) - Signature: {*/2,-/2,exp/2} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s} + 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(+) = {2} Following symbols are considered usable: {*,-,exp} TcT has computed the following interpretation: p(*) = [4] x2 + [0] p(+) = [1] x2 + [0] p(-) = [1] x1 + [4] p(0) = [0] p(exp) = [0] p(s) = [1] x1 + [0] Following rules are strictly oriented: -(x,0()) = [1] x + [4] > [1] x + [0] = x -(0(),y) = [4] > [0] = 0() Following rules are (at-least) weakly oriented: *(0(),y) = [4] y + [0] >= [0] = 0() *(s(x),y) = [4] y + [0] >= [4] y + [0] = +(y,*(x,y)) -(s(x),s(y)) = [1] x + [4] >= [1] x + [4] = -(x,y) exp(x,0()) = [0] >= [0] = s(0()) exp(x,s(y)) = [0] >= [0] = *(x,exp(x,y)) * Step 2: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: *(0(),y) -> 0() *(s(x),y) -> +(y,*(x,y)) -(s(x),s(y)) -> -(x,y) exp(x,0()) -> s(0()) exp(x,s(y)) -> *(x,exp(x,y)) - Weak TRS: -(x,0()) -> x -(0(),y) -> 0() - Signature: {*/2,-/2,exp/2} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s} + 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(*) = {2}, uargs(+) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(*) = [1] x2 + [1] p(+) = [1] x2 + [7] p(-) = [2] x1 + [4] x2 + [0] p(0) = [4] p(exp) = [1] x2 + [8] p(s) = [1] x1 + [1] Following rules are strictly oriented: -(s(x),s(y)) = [2] x + [4] y + [6] > [2] x + [4] y + [0] = -(x,y) exp(x,0()) = [12] > [5] = s(0()) Following rules are (at-least) weakly oriented: *(0(),y) = [1] y + [1] >= [4] = 0() *(s(x),y) = [1] y + [1] >= [1] y + [8] = +(y,*(x,y)) -(x,0()) = [2] x + [16] >= [1] x + [0] = x -(0(),y) = [4] y + [8] >= [4] = 0() exp(x,s(y)) = [1] y + [9] >= [1] y + [9] = *(x,exp(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 3: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: *(0(),y) -> 0() *(s(x),y) -> +(y,*(x,y)) exp(x,s(y)) -> *(x,exp(x,y)) - Weak TRS: -(x,0()) -> x -(0(),y) -> 0() -(s(x),s(y)) -> -(x,y) exp(x,0()) -> s(0()) - Signature: {*/2,-/2,exp/2} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s} + 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(*) = {2}, uargs(+) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(*) = [1] x2 + [0] p(+) = [1] x2 + [9] p(-) = [1] x1 + [2] x2 + [1] p(0) = [1] p(exp) = [6] x1 + [4] x2 + [12] p(s) = [1] x1 + [4] Following rules are strictly oriented: exp(x,s(y)) = [6] x + [4] y + [28] > [6] x + [4] y + [12] = *(x,exp(x,y)) Following rules are (at-least) weakly oriented: *(0(),y) = [1] y + [0] >= [1] = 0() *(s(x),y) = [1] y + [0] >= [1] y + [9] = +(y,*(x,y)) -(x,0()) = [1] x + [3] >= [1] x + [0] = x -(0(),y) = [2] y + [2] >= [1] = 0() -(s(x),s(y)) = [1] x + [2] y + [13] >= [1] x + [2] y + [1] = -(x,y) exp(x,0()) = [6] x + [16] >= [5] = s(0()) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: *(0(),y) -> 0() *(s(x),y) -> +(y,*(x,y)) - Weak TRS: -(x,0()) -> x -(0(),y) -> 0() -(s(x),s(y)) -> -(x,y) exp(x,0()) -> s(0()) exp(x,s(y)) -> *(x,exp(x,y)) - Signature: {*/2,-/2,exp/2} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s} + 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(*) = {2}, uargs(+) = {2} Following symbols are considered usable: all TcT has computed the following interpretation: p(*) = [1] x2 + [10] p(+) = [1] x2 + [0] p(-) = [2] x1 + [2] x2 + [6] p(0) = [0] p(exp) = [8] x2 + [14] p(s) = [1] x1 + [2] Following rules are strictly oriented: *(0(),y) = [1] y + [10] > [0] = 0() Following rules are (at-least) weakly oriented: *(s(x),y) = [1] y + [10] >= [1] y + [10] = +(y,*(x,y)) -(x,0()) = [2] x + [6] >= [1] x + [0] = x -(0(),y) = [2] y + [6] >= [0] = 0() -(s(x),s(y)) = [2] x + [2] y + [14] >= [2] x + [2] y + [6] = -(x,y) exp(x,0()) = [14] >= [2] = s(0()) exp(x,s(y)) = [8] y + [30] >= [8] y + [24] = *(x,exp(x,y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: *(s(x),y) -> +(y,*(x,y)) - Weak TRS: *(0(),y) -> 0() -(x,0()) -> x -(0(),y) -> 0() -(s(x),s(y)) -> -(x,y) exp(x,0()) -> s(0()) exp(x,s(y)) -> *(x,exp(x,y)) - Signature: {*/2,-/2,exp/2} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s} + 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(+) = {2} Following symbols are considered usable: {*,-,exp} TcT has computed the following interpretation: p(*) = 2 + x1 + x2 p(+) = x2 p(-) = x1*x2 + 2*x1^2 + x2 p(0) = 2 p(exp) = x1*x2 + 2*x2 p(s) = 1 + x1 Following rules are strictly oriented: *(s(x),y) = 3 + x + y > 2 + x + y = +(y,*(x,y)) Following rules are (at-least) weakly oriented: *(0(),y) = 4 + y >= 2 = 0() -(x,0()) = 2 + 2*x + 2*x^2 >= x = x -(0(),y) = 8 + 3*y >= 2 = 0() -(s(x),s(y)) = 4 + 5*x + x*y + 2*x^2 + 2*y >= x*y + 2*x^2 + y = -(x,y) exp(x,0()) = 4 + 2*x >= 3 = s(0()) exp(x,s(y)) = 2 + x + x*y + 2*y >= 2 + x + x*y + 2*y = *(x,exp(x,y)) * Step 6: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: *(0(),y) -> 0() *(s(x),y) -> +(y,*(x,y)) -(x,0()) -> x -(0(),y) -> 0() -(s(x),s(y)) -> -(x,y) exp(x,0()) -> s(0()) exp(x,s(y)) -> *(x,exp(x,y)) - Signature: {*/2,-/2,exp/2} / {+/2,0/0,s/1} - Obligation: innermost runtime complexity wrt. defined symbols {*,-,exp} and constructors {+,0,s} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))