WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
+ Considered Problem:
- Strict TRS:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
- Signature:
{a/0,activate/1,f/1,g/1} / {c/1,n__a/0,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a,activate,f,g} and constructors {c,n__a,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:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
- Signature:
{a/0,activate/1,f/1,g/1} / {c/1,n__a/0,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a,activate,f,g} and constructors {c,n__a,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:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
- Signature:
{a/0,activate/1,f/1,g/1} / {c/1,n__a/0,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a,activate,f,g} and constructors {c,n__a,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(f) = {1},
uargs(g) = {1}
Following symbols are considered usable:
{a,activate,f,g}
TcT has computed the following interpretation:
p(a) = 10
p(activate) = 13 + x1
p(c) = 0
p(f) = 8 + x1
p(g) = x1
p(n__a) = 6
p(n__f) = 8 + x1
p(n__g) = x1
Following rules are strictly oriented:
a() = 10
> 6
= n__a()
activate(X) = 13 + X
> X
= X
activate(n__a()) = 19
> 10
= a()
f(f(a())) = 26
> 0
= c(n__f(n__g(n__f(n__a()))))
Following rules are (at-least) weakly oriented:
activate(n__f(X)) = 21 + X
>= 21 + X
= f(activate(X))
activate(n__g(X)) = 13 + X
>= 13 + X
= g(activate(X))
f(X) = 8 + X
>= 8 + X
= n__f(X)
g(X) = X
>= X
= n__g(X)
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
g(X) -> n__g(X)
- Weak TRS:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
- Signature:
{a/0,activate/1,f/1,g/1} / {c/1,n__a/0,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a,activate,f,g} and constructors {c,n__a,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(f) = {1},
uargs(g) = {1}
Following symbols are considered usable:
{a,activate,f,g}
TcT has computed the following interpretation:
p(a) = 0
p(activate) = 2*x1
p(c) = 0
p(f) = 3 + x1
p(g) = 4 + x1
p(n__a) = 0
p(n__f) = 3 + x1
p(n__g) = 2 + x1
Following rules are strictly oriented:
activate(n__f(X)) = 6 + 2*X
> 3 + 2*X
= f(activate(X))
g(X) = 4 + X
> 2 + X
= n__g(X)
Following rules are (at-least) weakly oriented:
a() = 0
>= 0
= n__a()
activate(X) = 2*X
>= X
= X
activate(n__a()) = 0
>= 0
= a()
activate(n__g(X)) = 4 + 2*X
>= 4 + 2*X
= g(activate(X))
f(X) = 3 + X
>= 3 + X
= n__f(X)
f(f(a())) = 6
>= 0
= c(n__f(n__g(n__f(n__a()))))
** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
- Weak TRS:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
- Signature:
{a/0,activate/1,f/1,g/1} / {c/1,n__a/0,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a,activate,f,g} and constructors {c,n__a,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(f) = {1},
uargs(g) = {1}
Following symbols are considered usable:
{a,activate,f,g}
TcT has computed the following interpretation:
p(a) = 9
p(activate) = 8 + 2*x1
p(c) = x1
p(f) = 2 + x1
p(g) = 8 + x1
p(n__a) = 3
p(n__f) = 1 + x1
p(n__g) = 8 + x1
Following rules are strictly oriented:
activate(n__g(X)) = 24 + 2*X
> 16 + 2*X
= g(activate(X))
f(X) = 2 + X
> 1 + X
= n__f(X)
Following rules are (at-least) weakly oriented:
a() = 9
>= 3
= n__a()
activate(X) = 8 + 2*X
>= X
= X
activate(n__a()) = 14
>= 9
= a()
activate(n__f(X)) = 10 + 2*X
>= 10 + 2*X
= f(activate(X))
f(f(a())) = 13
>= 13
= c(n__f(n__g(n__f(n__a()))))
g(X) = 8 + X
>= 8 + X
= n__g(X)
** Step 1.b:4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(activate(X))
activate(n__g(X)) -> g(activate(X))
f(X) -> n__f(X)
f(f(a())) -> c(n__f(n__g(n__f(n__a()))))
g(X) -> n__g(X)
- Signature:
{a/0,activate/1,f/1,g/1} / {c/1,n__a/0,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a,activate,f,g} and constructors {c,n__a,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))