WORST_CASE(?,O(n^2)) * Step 1: InnermostRuleRemoval WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(n__s(X)) -> s(activate(X)) div(X1,X2) -> n__div(X1,X2) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) minus(X1,X2) -> n__minus(X1,X2) minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) s(X) -> n__s(X) - Signature: {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__div/2,n__minus/2,n__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__div,n__minus,n__s,true} + Applied Processor: InnermostRuleRemoval + Details: Arguments of following rules are not normal-forms. div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(n__div(n__minus(X,activate(Y)),n__s(activate(Y)))),n__0()) All above mentioned rules can be savely removed. * Step 2: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(n__s(X)) -> s(activate(X)) div(X1,X2) -> n__div(X1,X2) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) minus(X1,X2) -> n__minus(X1,X2) minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) s(X) -> n__s(X) - Signature: {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__div/2,n__minus/2,n__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__div,n__minus,n__s,true} + 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(geq) = {1,2}, uargs(minus) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [2] p(div) = [1] x1 + [1] x2 + [0] p(false) = [5] p(geq) = [1] x1 + [1] x2 + [7] p(if) = [5] x1 + [1] x2 + [1] x3 + [0] p(minus) = [1] x1 + [1] x2 + [7] p(n__0) = [0] p(n__div) = [1] x1 + [1] x2 + [0] p(n__minus) = [1] x1 + [1] x2 + [0] p(n__s) = [1] x1 + [0] p(s) = [1] x1 + [0] p(true) = [0] Following rules are strictly oriented: activate(X) = [1] X + [2] > [1] X + [0] = X activate(n__0()) = [2] > [0] = 0() geq(X,n__0()) = [1] X + [7] > [0] = true() geq(n__0(),n__s(Y)) = [1] Y + [7] > [5] = false() if(false(),X,Y) = [1] X + [1] Y + [25] > [1] Y + [2] = activate(Y) minus(X1,X2) = [1] X1 + [1] X2 + [7] > [1] X1 + [1] X2 + [0] = n__minus(X1,X2) minus(n__0(),Y) = [1] Y + [7] > [0] = 0() Following rules are (at-least) weakly oriented: 0() = [0] >= [0] = n__0() activate(n__div(X1,X2)) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [2] = div(activate(X1),X2) activate(n__minus(X1,X2)) = [1] X1 + [1] X2 + [2] >= [1] X1 + [1] X2 + [7] = minus(X1,X2) activate(n__s(X)) = [1] X + [2] >= [1] X + [2] = s(activate(X)) div(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__div(X1,X2) geq(n__s(X),n__s(Y)) = [1] X + [1] Y + [7] >= [1] X + [1] Y + [11] = geq(activate(X),activate(Y)) if(true(),X,Y) = [1] X + [1] Y + [0] >= [1] X + [2] = activate(X) minus(n__s(X),n__s(Y)) = [1] X + [1] Y + [7] >= [1] X + [1] Y + [11] = minus(activate(X),activate(Y)) s(X) = [1] X + [0] >= [1] X + [0] = n__s(X) 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() -> n__0() activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(n__s(X)) -> s(activate(X)) div(X1,X2) -> n__div(X1,X2) geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) if(true(),X,Y) -> activate(X) minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) s(X) -> n__s(X) - Weak TRS: activate(X) -> X activate(n__0()) -> 0() geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() if(false(),X,Y) -> activate(Y) minus(X1,X2) -> n__minus(X1,X2) minus(n__0(),Y) -> 0() - Signature: {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__div/2,n__minus/2,n__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__div,n__minus,n__s,true} + 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(geq) = {1,2}, uargs(minus) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [2] p(activate) = [1] x1 + [14] p(div) = [1] x1 + [1] x2 + [0] p(false) = [1] p(geq) = [1] x1 + [1] x2 + [0] p(if) = [13] x1 + [1] x2 + [1] x3 + [1] p(minus) = [1] x1 + [1] x2 + [1] p(n__0) = [1] p(n__div) = [1] x1 + [1] x2 + [0] p(n__minus) = [1] x1 + [1] x2 + [1] p(n__s) = [1] x1 + [0] p(s) = [1] x1 + [0] p(true) = [1] Following rules are strictly oriented: 0() = [2] > [1] = n__0() activate(n__minus(X1,X2)) = [1] X1 + [1] X2 + [15] > [1] X1 + [1] X2 + [1] = minus(X1,X2) Following rules are (at-least) weakly oriented: activate(X) = [1] X + [14] >= [1] X + [0] = X activate(n__0()) = [15] >= [2] = 0() activate(n__div(X1,X2)) = [1] X1 + [1] X2 + [14] >= [1] X1 + [1] X2 + [14] = div(activate(X1),X2) activate(n__s(X)) = [1] X + [14] >= [1] X + [14] = s(activate(X)) div(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__div(X1,X2) geq(X,n__0()) = [1] X + [1] >= [1] = true() geq(n__0(),n__s(Y)) = [1] Y + [1] >= [1] = false() geq(n__s(X),n__s(Y)) = [1] X + [1] Y + [0] >= [1] X + [1] Y + [28] = geq(activate(X),activate(Y)) if(false(),X,Y) = [1] X + [1] Y + [14] >= [1] Y + [14] = activate(Y) if(true(),X,Y) = [1] X + [1] Y + [14] >= [1] X + [14] = activate(X) minus(X1,X2) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = n__minus(X1,X2) minus(n__0(),Y) = [1] Y + [2] >= [2] = 0() minus(n__s(X),n__s(Y)) = [1] X + [1] Y + [1] >= [1] X + [1] Y + [29] = minus(activate(X),activate(Y)) s(X) = [1] X + [0] >= [1] X + [0] = n__s(X) 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: activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__s(X)) -> s(activate(X)) div(X1,X2) -> n__div(X1,X2) geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) if(true(),X,Y) -> activate(X) minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) s(X) -> n__s(X) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__minus(X1,X2)) -> minus(X1,X2) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() if(false(),X,Y) -> activate(Y) minus(X1,X2) -> n__minus(X1,X2) minus(n__0(),Y) -> 0() - Signature: {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__div/2,n__minus/2,n__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__div,n__minus,n__s,true} + 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(geq) = {1,2}, uargs(minus) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(div) = [1] x1 + [1] p(false) = [4] p(geq) = [1] x1 + [1] x2 + [4] p(if) = [1] x1 + [1] x2 + [9] x3 + [5] p(minus) = [1] x1 + [1] x2 + [1] p(n__0) = [0] p(n__div) = [1] x1 + [0] p(n__minus) = [1] x1 + [1] x2 + [1] p(n__s) = [1] x1 + [0] p(s) = [1] x1 + [0] p(true) = [4] Following rules are strictly oriented: div(X1,X2) = [1] X1 + [1] > [1] X1 + [0] = n__div(X1,X2) if(true(),X,Y) = [1] X + [9] Y + [9] > [1] X + [0] = activate(X) Following rules are (at-least) weakly oriented: 0() = [0] >= [0] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [0] >= [0] = 0() activate(n__div(X1,X2)) = [1] X1 + [0] >= [1] X1 + [1] = div(activate(X1),X2) activate(n__minus(X1,X2)) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = minus(X1,X2) activate(n__s(X)) = [1] X + [0] >= [1] X + [0] = s(activate(X)) geq(X,n__0()) = [1] X + [4] >= [4] = true() geq(n__0(),n__s(Y)) = [1] Y + [4] >= [4] = false() geq(n__s(X),n__s(Y)) = [1] X + [1] Y + [4] >= [1] X + [1] Y + [4] = geq(activate(X),activate(Y)) if(false(),X,Y) = [1] X + [9] Y + [9] >= [1] Y + [0] = activate(Y) minus(X1,X2) = [1] X1 + [1] X2 + [1] >= [1] X1 + [1] X2 + [1] = n__minus(X1,X2) minus(n__0(),Y) = [1] Y + [1] >= [0] = 0() minus(n__s(X),n__s(Y)) = [1] X + [1] Y + [1] >= [1] X + [1] Y + [1] = minus(activate(X),activate(Y)) s(X) = [1] X + [0] >= [1] X + [0] = n__s(X) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 5: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__s(X)) -> s(activate(X)) geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) s(X) -> n__s(X) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__minus(X1,X2)) -> minus(X1,X2) div(X1,X2) -> n__div(X1,X2) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) minus(X1,X2) -> n__minus(X1,X2) minus(n__0(),Y) -> 0() - Signature: {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__div/2,n__minus/2,n__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__div,n__minus,n__s,true} + 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(geq) = {1,2}, uargs(minus) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(div) = [1] x1 + [0] p(false) = [2] p(geq) = [1] x1 + [1] x2 + [2] p(if) = [4] x1 + [1] x2 + [1] x3 + [5] p(minus) = [1] x1 + [1] x2 + [0] p(n__0) = [0] p(n__div) = [1] x1 + [0] p(n__minus) = [1] x1 + [1] x2 + [0] p(n__s) = [1] x1 + [0] p(s) = [1] x1 + [4] p(true) = [1] Following rules are strictly oriented: s(X) = [1] X + [4] > [1] X + [0] = n__s(X) Following rules are (at-least) weakly oriented: 0() = [0] >= [0] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [0] >= [0] = 0() activate(n__div(X1,X2)) = [1] X1 + [0] >= [1] X1 + [0] = div(activate(X1),X2) activate(n__minus(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = minus(X1,X2) activate(n__s(X)) = [1] X + [0] >= [1] X + [4] = s(activate(X)) div(X1,X2) = [1] X1 + [0] >= [1] X1 + [0] = n__div(X1,X2) geq(X,n__0()) = [1] X + [2] >= [1] = true() geq(n__0(),n__s(Y)) = [1] Y + [2] >= [2] = false() geq(n__s(X),n__s(Y)) = [1] X + [1] Y + [2] >= [1] X + [1] Y + [2] = geq(activate(X),activate(Y)) if(false(),X,Y) = [1] X + [1] Y + [13] >= [1] Y + [0] = activate(Y) if(true(),X,Y) = [1] X + [1] Y + [9] >= [1] X + [0] = activate(X) minus(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__minus(X1,X2) minus(n__0(),Y) = [1] Y + [0] >= [0] = 0() minus(n__s(X),n__s(Y)) = [1] X + [1] Y + [0] >= [1] X + [1] Y + [0] = minus(activate(X),activate(Y)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__s(X)) -> s(activate(X)) geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__minus(X1,X2)) -> minus(X1,X2) div(X1,X2) -> n__div(X1,X2) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) minus(X1,X2) -> n__minus(X1,X2) minus(n__0(),Y) -> 0() s(X) -> n__s(X) - Signature: {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__div/2,n__minus/2,n__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__div,n__minus,n__s,true} + 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(geq) = {1,2}, uargs(minus) = {1,2}, uargs(s) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(0) = [0] p(activate) = [1] x1 + [0] p(div) = [1] x1 + [1] x2 + [5] p(false) = [1] p(geq) = [1] x1 + [1] x2 + [0] p(if) = [1] x2 + [1] x3 + [5] p(minus) = [1] x1 + [1] x2 + [0] p(n__0) = [0] p(n__div) = [1] x1 + [1] x2 + [5] p(n__minus) = [1] x1 + [1] x2 + [0] p(n__s) = [1] x1 + [1] p(s) = [1] x1 + [4] p(true) = [0] Following rules are strictly oriented: geq(n__s(X),n__s(Y)) = [1] X + [1] Y + [2] > [1] X + [1] Y + [0] = geq(activate(X),activate(Y)) minus(n__s(X),n__s(Y)) = [1] X + [1] Y + [2] > [1] X + [1] Y + [0] = minus(activate(X),activate(Y)) Following rules are (at-least) weakly oriented: 0() = [0] >= [0] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [0] >= [0] = 0() activate(n__div(X1,X2)) = [1] X1 + [1] X2 + [5] >= [1] X1 + [1] X2 + [5] = div(activate(X1),X2) activate(n__minus(X1,X2)) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = minus(X1,X2) activate(n__s(X)) = [1] X + [1] >= [1] X + [4] = s(activate(X)) div(X1,X2) = [1] X1 + [1] X2 + [5] >= [1] X1 + [1] X2 + [5] = n__div(X1,X2) geq(X,n__0()) = [1] X + [0] >= [0] = true() geq(n__0(),n__s(Y)) = [1] Y + [1] >= [1] = false() if(false(),X,Y) = [1] X + [1] Y + [5] >= [1] Y + [0] = activate(Y) if(true(),X,Y) = [1] X + [1] Y + [5] >= [1] X + [0] = activate(X) minus(X1,X2) = [1] X1 + [1] X2 + [0] >= [1] X1 + [1] X2 + [0] = n__minus(X1,X2) minus(n__0(),Y) = [1] Y + [0] >= [0] = 0() s(X) = [1] X + [4] >= [1] X + [1] = n__s(X) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 7: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__s(X)) -> s(activate(X)) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__minus(X1,X2)) -> minus(X1,X2) div(X1,X2) -> n__div(X1,X2) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) minus(X1,X2) -> n__minus(X1,X2) minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) s(X) -> n__s(X) - Signature: {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__div/2,n__minus/2,n__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__div,n__minus,n__s,true} + Applied Processor: NaturalMI {miDimension = 2, miDegree = 2, 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(div) = {1}, uargs(geq) = {1,2}, uargs(minus) = {1,2}, uargs(s) = {1} Following symbols are considered usable: {0,activate,div,geq,if,minus,s} TcT has computed the following interpretation: p(0) = [1] [0] p(activate) = [1 1] x1 + [0] [0 1] [0] p(div) = [1 0] x1 + [1] [0 1] [0] p(false) = [2] [1] p(geq) = [4 0] x1 + [2 0] x2 + [0] [3 4] [4 0] [0] p(if) = [4 1] x1 + [1 1] x2 + [4 1] x3 + [0] [4 1] [0 1] [4 1] [0] p(minus) = [1 3] x1 + [1 0] x2 + [0] [0 1] [0 0] [2] p(n__0) = [1] [0] p(n__div) = [1 0] x1 + [1] [0 1] [0] p(n__minus) = [1 3] x1 + [1 0] x2 + [0] [0 1] [0 0] [2] p(n__s) = [1 1] x1 + [0] [0 1] [1] p(s) = [1 1] x1 + [0] [0 1] [1] p(true) = [0] [4] Following rules are strictly oriented: activate(n__s(X)) = [1 2] X + [1] [0 1] [1] > [1 2] X + [0] [0 1] [1] = s(activate(X)) Following rules are (at-least) weakly oriented: 0() = [1] [0] >= [1] [0] = n__0() activate(X) = [1 1] X + [0] [0 1] [0] >= [1 0] X + [0] [0 1] [0] = X activate(n__0()) = [1] [0] >= [1] [0] = 0() activate(n__div(X1,X2)) = [1 1] X1 + [1] [0 1] [0] >= [1 1] X1 + [1] [0 1] [0] = div(activate(X1),X2) activate(n__minus(X1,X2)) = [1 4] X1 + [1 0] X2 + [2] [0 1] [0 0] [2] >= [1 3] X1 + [1 0] X2 + [0] [0 1] [0 0] [2] = minus(X1,X2) div(X1,X2) = [1 0] X1 + [1] [0 1] [0] >= [1 0] X1 + [1] [0 1] [0] = n__div(X1,X2) geq(X,n__0()) = [4 0] X + [2] [3 4] [4] >= [0] [4] = true() geq(n__0(),n__s(Y)) = [2 2] Y + [4] [4 4] [3] >= [2] [1] = false() geq(n__s(X),n__s(Y)) = [4 4] X + [2 2] Y + [0] [3 7] [4 4] [4] >= [4 4] X + [2 2] Y + [0] [3 7] [4 4] [0] = geq(activate(X),activate(Y)) if(false(),X,Y) = [1 1] X + [4 1] Y + [9] [0 1] [4 1] [9] >= [1 1] Y + [0] [0 1] [0] = activate(Y) if(true(),X,Y) = [1 1] X + [4 1] Y + [4] [0 1] [4 1] [4] >= [1 1] X + [0] [0 1] [0] = activate(X) minus(X1,X2) = [1 3] X1 + [1 0] X2 + [0] [0 1] [0 0] [2] >= [1 3] X1 + [1 0] X2 + [0] [0 1] [0 0] [2] = n__minus(X1,X2) minus(n__0(),Y) = [1 0] Y + [1] [0 0] [2] >= [1] [0] = 0() minus(n__s(X),n__s(Y)) = [1 4] X + [1 1] Y + [3] [0 1] [0 0] [3] >= [1 4] X + [1 1] Y + [0] [0 1] [0 0] [2] = minus(activate(X),activate(Y)) s(X) = [1 1] X + [0] [0 1] [1] >= [1 1] X + [0] [0 1] [1] = n__s(X) * Step 8: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: activate(n__div(X1,X2)) -> div(activate(X1),X2) - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__minus(X1,X2)) -> minus(X1,X2) activate(n__s(X)) -> s(activate(X)) div(X1,X2) -> n__div(X1,X2) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) minus(X1,X2) -> n__minus(X1,X2) minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) s(X) -> n__s(X) - Signature: {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__div/2,n__minus/2,n__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__div,n__minus,n__s,true} + Applied Processor: NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(div) = {1}, uargs(geq) = {1,2}, uargs(minus) = {1,2}, uargs(s) = {1} Following symbols are considered usable: {0,activate,div,geq,if,minus,s} TcT has computed the following interpretation: p(0) = [0] [1] [0] p(activate) = [1 0 2] [1] [0 1 0] x1 + [2] [0 0 1] [0] p(div) = [1 1 0] [1] [0 0 2] x1 + [1] [0 0 1] [2] p(false) = [0] [2] [1] p(geq) = [2 1 3] [1 1 2] [0] [0 0 2] x1 + [1 1 2] x2 + [0] [0 0 3] [0 0 0] [1] p(if) = [2 0 0] [1 0 2] [2 2 2] [2] [2 1 0] x1 + [2 2 0] x2 + [1 1 2] x3 + [2] [0 2 0] [0 2 2] [2 2 1] [0] p(minus) = [1 1 2] [1 1 2] [1] [0 0 0] x1 + [0 0 0] x2 + [1] [0 0 0] [0 0 0] [0] p(n__0) = [0] [1] [0] p(n__div) = [1 1 0] [1] [0 0 2] x1 + [0] [0 0 1] [2] p(n__minus) = [1 1 2] [1 1 2] [0] [0 0 0] x1 + [0 0 0] x2 + [1] [0 0 0] [0 0 0] [0] p(n__s) = [1 1 1] [0] [0 0 2] x1 + [1] [0 0 1] [1] p(s) = [1 1 1] [0] [0 0 2] x1 + [2] [0 0 1] [1] p(true) = [1] [1] [1] Following rules are strictly oriented: activate(n__div(X1,X2)) = [1 1 2] [6] [0 0 2] X1 + [2] [0 0 1] [2] > [1 1 2] [4] [0 0 2] X1 + [1] [0 0 1] [2] = div(activate(X1),X2) Following rules are (at-least) weakly oriented: 0() = [0] [1] [0] >= [0] [1] [0] = n__0() activate(X) = [1 0 2] [1] [0 1 0] X + [2] [0 0 1] [0] >= [1 0 0] [0] [0 1 0] X + [0] [0 0 1] [0] = X activate(n__0()) = [1] [3] [0] >= [0] [1] [0] = 0() activate(n__minus(X1,X2)) = [1 1 2] [1 1 2] [1] [0 0 0] X1 + [0 0 0] X2 + [3] [0 0 0] [0 0 0] [0] >= [1 1 2] [1 1 2] [1] [0 0 0] X1 + [0 0 0] X2 + [1] [0 0 0] [0 0 0] [0] = minus(X1,X2) activate(n__s(X)) = [1 1 3] [3] [0 0 2] X + [3] [0 0 1] [1] >= [1 1 3] [3] [0 0 2] X + [2] [0 0 1] [1] = s(activate(X)) div(X1,X2) = [1 1 0] [1] [0 0 2] X1 + [1] [0 0 1] [2] >= [1 1 0] [1] [0 0 2] X1 + [0] [0 0 1] [2] = n__div(X1,X2) geq(X,n__0()) = [2 1 3] [1] [0 0 2] X + [1] [0 0 3] [1] >= [1] [1] [1] = true() geq(n__0(),n__s(Y)) = [1 1 5] [4] [1 1 5] Y + [3] [0 0 0] [1] >= [0] [2] [1] = false() geq(n__s(X),n__s(Y)) = [2 2 7] [1 1 5] [7] [0 0 2] X + [1 1 5] Y + [5] [0 0 3] [0 0 0] [4] >= [2 1 7] [1 1 4] [7] [0 0 2] X + [1 1 4] Y + [3] [0 0 3] [0 0 0] [1] = geq(activate(X),activate(Y)) if(false(),X,Y) = [1 0 2] [2 2 2] [2] [2 2 0] X + [1 1 2] Y + [4] [0 2 2] [2 2 1] [4] >= [1 0 2] [1] [0 1 0] Y + [2] [0 0 1] [0] = activate(Y) if(true(),X,Y) = [1 0 2] [2 2 2] [4] [2 2 0] X + [1 1 2] Y + [5] [0 2 2] [2 2 1] [2] >= [1 0 2] [1] [0 1 0] X + [2] [0 0 1] [0] = activate(X) minus(X1,X2) = [1 1 2] [1 1 2] [1] [0 0 0] X1 + [0 0 0] X2 + [1] [0 0 0] [0 0 0] [0] >= [1 1 2] [1 1 2] [0] [0 0 0] X1 + [0 0 0] X2 + [1] [0 0 0] [0 0 0] [0] = n__minus(X1,X2) minus(n__0(),Y) = [1 1 2] [2] [0 0 0] Y + [1] [0 0 0] [0] >= [0] [1] [0] = 0() minus(n__s(X),n__s(Y)) = [1 1 5] [1 1 5] [7] [0 0 0] X + [0 0 0] Y + [1] [0 0 0] [0 0 0] [0] >= [1 1 4] [1 1 4] [7] [0 0 0] X + [0 0 0] Y + [1] [0 0 0] [0 0 0] [0] = minus(activate(X),activate(Y)) s(X) = [1 1 1] [0] [0 0 2] X + [2] [0 0 1] [1] >= [1 1 1] [0] [0 0 2] X + [1] [0 0 1] [1] = n__s(X) * Step 9: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__div(X1,X2)) -> div(activate(X1),X2) activate(n__minus(X1,X2)) -> minus(X1,X2) activate(n__s(X)) -> s(activate(X)) div(X1,X2) -> n__div(X1,X2) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) if(false(),X,Y) -> activate(Y) if(true(),X,Y) -> activate(X) minus(X1,X2) -> n__minus(X1,X2) minus(n__0(),Y) -> 0() minus(n__s(X),n__s(Y)) -> minus(activate(X),activate(Y)) s(X) -> n__s(X) - Signature: {0/0,activate/1,div/2,geq/2,if/3,minus/2,s/1} / {false/0,n__0/0,n__div/2,n__minus/2,n__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__div,n__minus,n__s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))