WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(n__g(n__f(X))))
g(X) -> n__g(X)
h(X) -> c(n__d(X))
- Signature:
{activate/1,c/1,d/1,f/1,g/1,h/1} / {n__d/1,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,c,d,f,g,h} and constructors {n__d,n__f,n__g}
+ Applied Processor:
Sum {left = someStrategy, right = someStrategy}
+ Details:
()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
+ Considered Problem:
- Strict TRS:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(n__g(n__f(X))))
g(X) -> n__g(X)
h(X) -> c(n__d(X))
- Signature:
{activate/1,c/1,d/1,f/1,g/1,h/1} / {n__d/1,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,c,d,f,g,h} and constructors {n__d,n__f,n__g}
+ Applied Processor:
DecreasingLoops {bound = AnyLoop, narrow = 10}
+ Details:
The system has following decreasing Loops:
activate(x){x -> n__f(x)} =
activate(n__f(x)) ->^+ f(activate(x))
= C[activate(x) = activate(x){}]
** Step 1.b:1: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(n__g(n__f(X))))
g(X) -> n__g(X)
h(X) -> c(n__d(X))
- Signature:
{activate/1,c/1,d/1,f/1,g/1,h/1} / {n__d/1,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,c,d,f,g,h} and constructors {n__d,n__f,n__g}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(d) = {1},
uargs(f) = {1}
Following symbols are considered usable:
{activate,c,d,f,g,h}
TcT has computed the following interpretation:
p(activate) = 2*x1
p(c) = 8*x1
p(d) = 2*x1
p(f) = x1
p(g) = 0
p(h) = 10 + 14*x1
p(n__d) = x1
p(n__f) = x1
p(n__g) = 0
Following rules are strictly oriented:
h(X) = 10 + 14*X
> 8*X
= c(n__d(X))
Following rules are (at-least) weakly oriented:
activate(X) = 2*X
>= X
= X
activate(n__d(X)) = 2*X
>= 2*X
= d(X)
activate(n__f(X)) = 2*X
>= 2*X
= f(activate(X))
activate(n__g(X)) = 0
>= 0
= g(X)
c(X) = 8*X
>= 4*X
= d(activate(X))
d(X) = 2*X
>= X
= n__d(X)
f(X) = X
>= X
= n__f(X)
f(f(X)) = X
>= 0
= c(n__f(n__g(n__f(X))))
g(X) = 0
>= 0
= n__g(X)
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(n__g(n__f(X))))
g(X) -> n__g(X)
- Weak TRS:
h(X) -> c(n__d(X))
- Signature:
{activate/1,c/1,d/1,f/1,g/1,h/1} / {n__d/1,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,c,d,f,g,h} and constructors {n__d,n__f,n__g}
+ 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(d) = {1},
uargs(f) = {1}
Following symbols are considered usable:
{activate,c,d,f,g,h}
TcT has computed the following interpretation:
p(activate) = 3*x1
p(c) = 3*x1
p(d) = x1
p(f) = 3 + x1
p(g) = 0
p(h) = 1 + 4*x1
p(n__d) = x1
p(n__f) = 2 + x1
p(n__g) = 0
Following rules are strictly oriented:
activate(n__f(X)) = 6 + 3*X
> 3 + 3*X
= f(activate(X))
f(X) = 3 + X
> 2 + X
= n__f(X)
Following rules are (at-least) weakly oriented:
activate(X) = 3*X
>= X
= X
activate(n__d(X)) = 3*X
>= X
= d(X)
activate(n__g(X)) = 0
>= 0
= g(X)
c(X) = 3*X
>= 3*X
= d(activate(X))
d(X) = X
>= X
= n__d(X)
f(f(X)) = 6 + X
>= 6
= c(n__f(n__g(n__f(X))))
g(X) = 0
>= 0
= n__g(X)
h(X) = 1 + 4*X
>= 3*X
= c(n__d(X))
** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__g(X)) -> g(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(f(X)) -> c(n__f(n__g(n__f(X))))
g(X) -> n__g(X)
- Weak TRS:
activate(n__f(X)) -> f(activate(X))
f(X) -> n__f(X)
h(X) -> c(n__d(X))
- Signature:
{activate/1,c/1,d/1,f/1,g/1,h/1} / {n__d/1,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,c,d,f,g,h} and constructors {n__d,n__f,n__g}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(d) = {1},
uargs(f) = {1}
Following symbols are considered usable:
{activate,c,d,f,g,h}
TcT has computed the following interpretation:
p(activate) = 2*x1
p(c) = 2 + 2*x1
p(d) = 2 + x1
p(f) = 3 + x1
p(g) = 0
p(h) = 9 + 2*x1
p(n__d) = 2 + x1
p(n__f) = 2 + x1
p(n__g) = 0
Following rules are strictly oriented:
activate(n__d(X)) = 4 + 2*X
> 2 + X
= d(X)
Following rules are (at-least) weakly oriented:
activate(X) = 2*X
>= X
= X
activate(n__f(X)) = 4 + 2*X
>= 3 + 2*X
= f(activate(X))
activate(n__g(X)) = 0
>= 0
= g(X)
c(X) = 2 + 2*X
>= 2 + 2*X
= d(activate(X))
d(X) = 2 + X
>= 2 + X
= n__d(X)
f(X) = 3 + X
>= 2 + X
= n__f(X)
f(f(X)) = 6 + X
>= 6
= c(n__f(n__g(n__f(X))))
g(X) = 0
>= 0
= n__g(X)
h(X) = 9 + 2*X
>= 6 + 2*X
= c(n__d(X))
** Step 1.b:4: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(X) -> X
activate(n__g(X)) -> g(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(f(X)) -> c(n__f(n__g(n__f(X))))
g(X) -> n__g(X)
- Weak TRS:
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(activate(X))
f(X) -> n__f(X)
h(X) -> c(n__d(X))
- Signature:
{activate/1,c/1,d/1,f/1,g/1,h/1} / {n__d/1,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,c,d,f,g,h} and constructors {n__d,n__f,n__g}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(d) = {1},
uargs(f) = {1}
Following symbols are considered usable:
{activate,c,d,f,g,h}
TcT has computed the following interpretation:
p(activate) = 1 + 8*x1
p(c) = 2 + 12*x1
p(d) = x1
p(f) = 8 + x1
p(g) = 1
p(h) = 5 + 12*x1
p(n__d) = x1
p(n__f) = 1 + x1
p(n__g) = 0
Following rules are strictly oriented:
activate(X) = 1 + 8*X
> X
= X
c(X) = 2 + 12*X
> 1 + 8*X
= d(activate(X))
f(f(X)) = 16 + X
> 14
= c(n__f(n__g(n__f(X))))
g(X) = 1
> 0
= n__g(X)
Following rules are (at-least) weakly oriented:
activate(n__d(X)) = 1 + 8*X
>= X
= d(X)
activate(n__f(X)) = 9 + 8*X
>= 9 + 8*X
= f(activate(X))
activate(n__g(X)) = 1
>= 1
= g(X)
d(X) = X
>= X
= n__d(X)
f(X) = 8 + X
>= 1 + X
= n__f(X)
h(X) = 5 + 12*X
>= 2 + 12*X
= c(n__d(X))
** Step 1.b:5: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(n__g(X)) -> g(X)
d(X) -> n__d(X)
- Weak TRS:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(activate(X))
c(X) -> d(activate(X))
f(X) -> n__f(X)
f(f(X)) -> c(n__f(n__g(n__f(X))))
g(X) -> n__g(X)
h(X) -> c(n__d(X))
- Signature:
{activate/1,c/1,d/1,f/1,g/1,h/1} / {n__d/1,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,c,d,f,g,h} and constructors {n__d,n__f,n__g}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(d) = {1},
uargs(f) = {1}
Following symbols are considered usable:
{activate,c,d,f,g,h}
TcT has computed the following interpretation:
p(activate) = 8*x1
p(c) = 1 + 8*x1
p(d) = x1
p(f) = 13 + x1
p(g) = 4
p(h) = 8 + 11*x1
p(n__d) = x1
p(n__f) = 2 + x1
p(n__g) = 1
Following rules are strictly oriented:
activate(n__g(X)) = 8
> 4
= g(X)
Following rules are (at-least) weakly oriented:
activate(X) = 8*X
>= X
= X
activate(n__d(X)) = 8*X
>= X
= d(X)
activate(n__f(X)) = 16 + 8*X
>= 13 + 8*X
= f(activate(X))
c(X) = 1 + 8*X
>= 8*X
= d(activate(X))
d(X) = X
>= X
= n__d(X)
f(X) = 13 + X
>= 2 + X
= n__f(X)
f(f(X)) = 26 + X
>= 25
= c(n__f(n__g(n__f(X))))
g(X) = 4
>= 1
= n__g(X)
h(X) = 8 + 11*X
>= 1 + 8*X
= c(n__d(X))
** Step 1.b:6: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
d(X) -> n__d(X)
- Weak TRS:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(X)
c(X) -> d(activate(X))
f(X) -> n__f(X)
f(f(X)) -> c(n__f(n__g(n__f(X))))
g(X) -> n__g(X)
h(X) -> c(n__d(X))
- Signature:
{activate/1,c/1,d/1,f/1,g/1,h/1} / {n__d/1,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,c,d,f,g,h} and constructors {n__d,n__f,n__g}
+ Applied Processor:
NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(linear):
The following argument positions are considered usable:
uargs(d) = {1},
uargs(f) = {1}
Following symbols are considered usable:
{activate,c,d,f,g,h}
TcT has computed the following interpretation:
p(activate) = 2 + 8*x1
p(c) = 5 + 8*x1
p(d) = 3 + x1
p(f) = 15 + x1
p(g) = 0
p(h) = 13 + 10*x1
p(n__d) = 1 + x1
p(n__f) = 2 + x1
p(n__g) = 0
Following rules are strictly oriented:
d(X) = 3 + X
> 1 + X
= n__d(X)
Following rules are (at-least) weakly oriented:
activate(X) = 2 + 8*X
>= X
= X
activate(n__d(X)) = 10 + 8*X
>= 3 + X
= d(X)
activate(n__f(X)) = 18 + 8*X
>= 17 + 8*X
= f(activate(X))
activate(n__g(X)) = 2
>= 0
= g(X)
c(X) = 5 + 8*X
>= 5 + 8*X
= d(activate(X))
f(X) = 15 + X
>= 2 + X
= n__f(X)
f(f(X)) = 30 + X
>= 21
= c(n__f(n__g(n__f(X))))
g(X) = 0
>= 0
= n__g(X)
h(X) = 13 + 10*X
>= 13 + 8*X
= c(n__d(X))
** Step 1.b:7: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
activate(X) -> X
activate(n__d(X)) -> d(X)
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(X)
c(X) -> d(activate(X))
d(X) -> n__d(X)
f(X) -> n__f(X)
f(f(X)) -> c(n__f(n__g(n__f(X))))
g(X) -> n__g(X)
h(X) -> c(n__d(X))
- Signature:
{activate/1,c/1,d/1,f/1,g/1,h/1} / {n__d/1,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {activate,c,d,f,g,h} and constructors {n__d,n__f,n__g}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(Omega(n^1),O(n^1))