* Step 1: Sum 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:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
* Step 2: 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 3: 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 4: 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))