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 + [5] p(div) = [1] x1 + [1] x2 + [7] p(false) = [0] p(geq) = [1] x1 + [1] x2 + [8] p(if) = [7] x1 + [1] x2 + [3] x3 + [1] p(minus) = [1] x1 + [1] x2 + [8] p(n__0) = [11] p(n__div) = [1] x1 + [1] x2 + [3] p(n__minus) = [1] x1 + [1] x2 + [2] p(n__s) = [1] x1 + [0] p(s) = [1] x1 + [0] p(true) = [4] Following rules are strictly oriented: activate(X) = [1] X + [5] > [1] X + [0] = X activate(n__0()) = [16] > [0] = 0() div(X1,X2) = [1] X1 + [1] X2 + [7] > [1] X1 + [1] X2 + [3] = n__div(X1,X2) geq(X,n__0()) = [1] X + [19] > [4] = true() geq(n__0(),n__s(Y)) = [1] Y + [19] > [0] = false() if(true(),X,Y) = [1] X + [3] Y + [29] > [1] X + [5] = activate(X) minus(X1,X2) = [1] X1 + [1] X2 + [8] > [1] X1 + [1] X2 + [2] = n__minus(X1,X2) minus(n__0(),Y) = [1] Y + [19] > [0] = 0() Following rules are (at-least) weakly oriented: 0() = [0] >= [11] = n__0() activate(n__div(X1,X2)) = [1] X1 + [1] X2 + [8] >= [1] X1 + [1] X2 + [12] = div(activate(X1),X2) activate(n__minus(X1,X2)) = [1] X1 + [1] X2 + [7] >= [1] X1 + [1] X2 + [8] = minus(X1,X2) activate(n__s(X)) = [1] X + [5] >= [1] X + [5] = s(activate(X)) geq(n__s(X),n__s(Y)) = [1] X + [1] Y + [8] >= [1] X + [1] Y + [18] = geq(activate(X),activate(Y)) if(false(),X,Y) = [1] X + [3] Y + [1] >= [1] Y + [5] = activate(Y) minus(n__s(X),n__s(Y)) = [1] X + [1] Y + [8] >= [1] X + [1] Y + [18] = 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)) geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) if(false(),X,Y) -> activate(Y) 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() div(X1,X2) -> n__div(X1,X2) geq(X,n__0()) -> true() geq(n__0(),n__s(Y)) -> false() 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) = [10] p(activate) = [1] x1 + [14] p(div) = [1] x1 + [0] p(false) = [15] p(geq) = [1] x1 + [1] x2 + [3] p(if) = [1] x2 + [1] x3 + [14] p(minus) = [1] x1 + [1] x2 + [2] p(n__0) = [8] p(n__div) = [1] x1 + [0] p(n__minus) = [1] x1 + [1] x2 + [2] p(n__s) = [1] x1 + [4] p(s) = [1] x1 + [0] p(true) = [11] Following rules are strictly oriented: 0() = [10] > [8] = n__0() activate(n__minus(X1,X2)) = [1] X1 + [1] X2 + [16] > [1] X1 + [1] X2 + [2] = minus(X1,X2) activate(n__s(X)) = [1] X + [18] > [1] X + [14] = s(activate(X)) Following rules are (at-least) weakly oriented: activate(X) = [1] X + [14] >= [1] X + [0] = X activate(n__0()) = [22] >= [10] = 0() activate(n__div(X1,X2)) = [1] X1 + [14] >= [1] X1 + [14] = div(activate(X1),X2) div(X1,X2) = [1] X1 + [0] >= [1] X1 + [0] = n__div(X1,X2) geq(X,n__0()) = [1] X + [11] >= [11] = true() geq(n__0(),n__s(Y)) = [1] Y + [15] >= [15] = false() geq(n__s(X),n__s(Y)) = [1] X + [1] Y + [11] >= [1] X + [1] Y + [31] = 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 + [2] >= [1] X1 + [1] X2 + [2] = n__minus(X1,X2) minus(n__0(),Y) = [1] Y + [10] >= [10] = 0() minus(n__s(X),n__s(Y)) = [1] X + [1] Y + [10] >= [1] X + [1] Y + [30] = minus(activate(X),activate(Y)) s(X) = [1] X + [0] >= [1] X + [4] = n__s(X) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 4: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: activate(n__div(X1,X2)) -> div(activate(X1),X2) geq(n__s(X),n__s(Y)) -> geq(activate(X),activate(Y)) if(false(),X,Y) -> 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) 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() 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: 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(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) = [3] p(activate) = [1] x1 + [0] p(div) = [1] x1 + [8] p(false) = [2] p(geq) = [1] x1 + [4] x2 + [0] p(if) = [8] x1 + [1] x2 + [1] x3 + [0] p(minus) = [1] x1 + [1] x2 + [1] p(n__0) = [3] p(n__div) = [1] x1 + [8] p(n__minus) = [1] x1 + [1] x2 + [1] p(n__s) = [1] x1 + [0] p(s) = [1] x1 + [0] p(true) = [0] Following rules are strictly oriented: if(false(),X,Y) = [1] X + [1] Y + [16] > [1] Y + [0] = activate(Y) Following rules are (at-least) weakly oriented: 0() = [3] >= [3] = n__0() activate(X) = [1] X + [0] >= [1] X + [0] = X activate(n__0()) = [3] >= [3] = 0() activate(n__div(X1,X2)) = [1] X1 + [8] >= [1] X1 + [8] = 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)) div(X1,X2) = [1] X1 + [8] >= [1] X1 + [8] = n__div(X1,X2) geq(X,n__0()) = [1] X + [12] >= [0] = true() geq(n__0(),n__s(Y)) = [4] Y + [3] >= [2] = false() geq(n__s(X),n__s(Y)) = [1] X + [4] Y + [0] >= [1] X + [4] Y + [0] = geq(activate(X),activate(Y)) if(true(),X,Y) = [1] X + [1] Y + [0] >= [1] X + [0] = 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 + [4] >= [3] = 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) * Step 5: WeightGap WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: activate(n__div(X1,X2)) -> div(activate(X1),X2) 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) 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() 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 + [1] x2 + [0] p(false) = [5] p(geq) = [1] x1 + [1] x2 + [0] p(if) = [3] x1 + [1] x2 + [1] x3 + [0] p(minus) = [1] x1 + [1] x2 + [0] 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 + [5] p(s) = [1] x1 + [5] p(true) = [0] Following rules are strictly oriented: geq(n__s(X),n__s(Y)) = [1] X + [1] Y + [10] > [1] X + [1] Y + [0] = geq(activate(X),activate(Y)) minus(n__s(X),n__s(Y)) = [1] X + [1] Y + [10] > [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 + [0] >= [1] X1 + [1] X2 + [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 + [5] >= [1] X + [5] = 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 + [0] >= [0] = true() geq(n__0(),n__s(Y)) = [1] Y + [5] >= [5] = false() if(false(),X,Y) = [1] X + [1] Y + [15] >= [1] Y + [0] = activate(Y) if(true(),X,Y) = [1] X + [1] Y + [0] >= [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 + [5] >= [1] X + [5] = n__s(X) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 6: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: activate(n__div(X1,X2)) -> div(activate(X1),X2) 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) 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)) - 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) = [0] [4] p(activate) = [1 2] x1 + [0] [0 1] [0] p(div) = [1 0] x1 + [0] [0 1] [1] p(false) = [0] [1] p(geq) = [2 0] x1 + [1 1] x2 + [4] [2 2] [0 2] [4] p(if) = [4 0] x1 + [1 3] x2 + [4 4] x3 + [1] [6 2] [4 1] [0 2] [0] p(minus) = [1 2] x1 + [1 0] x2 + [1] [0 1] [0 0] [2] p(n__0) = [0] [4] p(n__div) = [1 0] x1 + [0] [0 1] [1] p(n__minus) = [1 0] x1 + [1 0] x2 + [0] [0 1] [0 0] [2] p(n__s) = [1 4] x1 + [2] [0 1] [0] p(s) = [1 4] x1 + [2] [0 1] [0] p(true) = [2] [1] Following rules are strictly oriented: activate(n__div(X1,X2)) = [1 2] X1 + [2] [0 1] [1] > [1 2] X1 + [0] [0 1] [1] = div(activate(X1),X2) Following rules are (at-least) weakly oriented: 0() = [0] [4] >= [0] [4] = n__0() activate(X) = [1 2] X + [0] [0 1] [0] >= [1 0] X + [0] [0 1] [0] = X activate(n__0()) = [8] [4] >= [0] [4] = 0() activate(n__minus(X1,X2)) = [1 2] X1 + [1 0] X2 + [4] [0 1] [0 0] [2] >= [1 2] X1 + [1 0] X2 + [1] [0 1] [0 0] [2] = minus(X1,X2) activate(n__s(X)) = [1 6] X + [2] [0 1] [0] >= [1 6] X + [2] [0 1] [0] = s(activate(X)) div(X1,X2) = [1 0] X1 + [0] [0 1] [1] >= [1 0] X1 + [0] [0 1] [1] = n__div(X1,X2) geq(X,n__0()) = [2 0] X + [8] [2 2] [12] >= [2] [1] = true() geq(n__0(),n__s(Y)) = [1 5] Y + [6] [0 2] [12] >= [0] [1] = false() geq(n__s(X),n__s(Y)) = [2 8] X + [1 5] Y + [10] [2 10] [0 2] [8] >= [2 4] X + [1 3] Y + [4] [2 6] [0 2] [4] = geq(activate(X),activate(Y)) if(false(),X,Y) = [1 3] X + [4 4] Y + [1] [4 1] [0 2] [2] >= [1 2] Y + [0] [0 1] [0] = activate(Y) if(true(),X,Y) = [1 3] X + [4 4] Y + [9] [4 1] [0 2] [14] >= [1 2] X + [0] [0 1] [0] = activate(X) minus(X1,X2) = [1 2] X1 + [1 0] X2 + [1] [0 1] [0 0] [2] >= [1 0] X1 + [1 0] X2 + [0] [0 1] [0 0] [2] = n__minus(X1,X2) minus(n__0(),Y) = [1 0] Y + [9] [0 0] [6] >= [0] [4] = 0() minus(n__s(X),n__s(Y)) = [1 6] X + [1 4] Y + [5] [0 1] [0 0] [2] >= [1 4] X + [1 2] Y + [1] [0 1] [0 0] [2] = minus(activate(X),activate(Y)) s(X) = [1 4] X + [2] [0 1] [0] >= [1 4] X + [2] [0 1] [0] = n__s(X) * Step 7: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: s(X) -> n__s(X) - 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)) - 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 4] x1 + [0] [0 1] [0] p(div) = [1 0] x1 + [4] [0 1] [1] p(false) = [0] [2] p(geq) = [1 1] x1 + [1 0] x2 + [0] [0 1] [2 3] [7] p(if) = [0 4] x1 + [4 6] x2 + [1 4] x3 + [5] [1 0] [4 4] [0 4] [4] p(minus) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(n__0) = [1] [0] p(n__div) = [1 0] x1 + [0] [0 1] [1] p(n__minus) = [1 0] x1 + [1 0] x2 + [0] [0 0] [0 0] [0] p(n__s) = [1 4] x1 + [0] [0 1] [1] p(s) = [1 4] x1 + [4] [0 1] [1] p(true) = [0] [0] Following rules are strictly oriented: s(X) = [1 4] X + [4] [0 1] [1] > [1 4] X + [0] [0 1] [1] = n__s(X) Following rules are (at-least) weakly oriented: 0() = [1] [0] >= [1] [0] = n__0() activate(X) = [1 4] 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 4] X1 + [4] [0 1] [1] >= [1 4] X1 + [4] [0 1] [1] = div(activate(X1),X2) activate(n__minus(X1,X2)) = [1 0] X1 + [1 0] X2 + [0] [0 0] [0 0] [0] >= [1 0] X1 + [1 0] X2 + [0] [0 0] [0 0] [0] = minus(X1,X2) activate(n__s(X)) = [1 8] X + [4] [0 1] [1] >= [1 8] X + [4] [0 1] [1] = s(activate(X)) div(X1,X2) = [1 0] X1 + [4] [0 1] [1] >= [1 0] X1 + [0] [0 1] [1] = n__div(X1,X2) geq(X,n__0()) = [1 1] X + [1] [0 1] [9] >= [0] [0] = true() geq(n__0(),n__s(Y)) = [1 4] Y + [1] [2 11] [10] >= [0] [2] = false() geq(n__s(X),n__s(Y)) = [1 5] X + [1 4] Y + [1] [0 1] [2 11] [11] >= [1 5] X + [1 4] Y + [0] [0 1] [2 11] [7] = geq(activate(X),activate(Y)) if(false(),X,Y) = [4 6] X + [1 4] Y + [13] [4 4] [0 4] [4] >= [1 4] Y + [0] [0 1] [0] = activate(Y) if(true(),X,Y) = [4 6] X + [1 4] Y + [5] [4 4] [0 4] [4] >= [1 4] X + [0] [0 1] [0] = activate(X) minus(X1,X2) = [1 0] X1 + [1 0] X2 + [0] [0 0] [0 0] [0] >= [1 0] X1 + [1 0] X2 + [0] [0 0] [0 0] [0] = n__minus(X1,X2) minus(n__0(),Y) = [1 0] Y + [1] [0 0] [0] >= [1] [0] = 0() minus(n__s(X),n__s(Y)) = [1 4] X + [1 4] Y + [0] [0 0] [0 0] [0] >= [1 4] X + [1 4] Y + [0] [0 0] [0 0] [0] = minus(activate(X),activate(Y)) * Step 8: 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))