WORST_CASE(?,O(n^1)) * Step 1: InnermostRuleRemoval WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__s(X)) -> s(X) div(0(),n__s(Y)) -> 0() div(s(X),n__s(Y)) -> if(geq(X,activate(Y)),n__s(div(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(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__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,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(div(minus(X,activate(Y)),n__s(activate(Y)))),n__0()) All above mentioned rules can be savely removed. * Step 2: Bounds WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__s(X)) -> s(X) 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(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__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__s,true} + Applied Processor: Bounds {initialAutomaton = minimal, enrichment = match} + Details: The problem is match-bounded by 4. The enriched problem is compatible with follwoing automaton. 0_0() -> 1 0_1() -> 1 0_1() -> 3 0_1() -> 4 0_1() -> 5 0_1() -> 6 0_1() -> 7 0_1() -> 8 0_2() -> 1 0_3() -> 1 activate_0(2) -> 1 activate_1(2) -> 1 activate_1(2) -> 3 activate_1(2) -> 4 activate_2(2) -> 5 activate_2(2) -> 6 activate_3(2) -> 7 activate_3(2) -> 8 div_0(2,2) -> 1 false_0() -> 1 false_0() -> 2 false_0() -> 3 false_0() -> 4 false_0() -> 5 false_0() -> 6 false_0() -> 7 false_0() -> 8 false_1() -> 1 false_2() -> 1 false_3() -> 1 geq_0(2,2) -> 1 geq_1(3,4) -> 1 geq_2(5,6) -> 1 geq_3(7,8) -> 1 if_0(2,2,2) -> 1 minus_0(2,2) -> 1 minus_1(4,4) -> 1 minus_2(6,6) -> 1 minus_3(8,8) -> 1 n__0_0() -> 1 n__0_0() -> 2 n__0_0() -> 3 n__0_0() -> 4 n__0_0() -> 5 n__0_0() -> 6 n__0_0() -> 7 n__0_0() -> 8 n__0_1() -> 1 n__0_2() -> 1 n__0_2() -> 3 n__0_2() -> 4 n__0_2() -> 5 n__0_2() -> 6 n__0_2() -> 7 n__0_2() -> 8 n__0_3() -> 1 n__0_4() -> 1 n__s_0(2) -> 1 n__s_0(2) -> 2 n__s_0(2) -> 3 n__s_0(2) -> 4 n__s_0(2) -> 5 n__s_0(2) -> 6 n__s_0(2) -> 7 n__s_0(2) -> 8 n__s_1(2) -> 1 n__s_2(2) -> 1 n__s_2(2) -> 3 n__s_2(2) -> 4 n__s_2(2) -> 5 n__s_2(2) -> 6 n__s_2(2) -> 7 n__s_2(2) -> 8 s_0(2) -> 1 s_1(2) -> 1 s_1(2) -> 3 s_1(2) -> 4 s_1(2) -> 5 s_1(2) -> 6 s_1(2) -> 7 s_1(2) -> 8 true_0() -> 1 true_0() -> 2 true_0() -> 3 true_0() -> 4 true_0() -> 5 true_0() -> 6 true_0() -> 7 true_0() -> 8 true_1() -> 1 true_2() -> 1 true_3() -> 1 2 -> 1 2 -> 3 2 -> 4 2 -> 5 2 -> 6 2 -> 7 2 -> 8 * Step 3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: 0() -> n__0() activate(X) -> X activate(n__0()) -> 0() activate(n__s(X)) -> s(X) 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(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__s/1,true/0} - Obligation: innermost runtime complexity wrt. defined symbols {0,activate,div,geq,if,minus,s} and constructors {false ,n__0,n__s,true} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))