* Step 1: ToInnermost WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(X)
activate(n__g(X)) -> g(X)
f(X) -> n__f(X)
f(n__f(n__a())) -> f(n__g(f(n__a())))
g(X) -> n__g(X)
- Signature:
{a/0,activate/1,f/1,g/1} / {n__a/0,n__f/1,n__g/1}
- Obligation:
runtime complexity wrt. defined symbols {a,activate,f,g} and constructors {n__a,n__f,n__g}
+ Applied Processor:
ToInnermost
+ Details:
switch to innermost, as the system is overlay and right linear and does not contain weak rules
* Step 2: DependencyPairs WORST_CASE(?,O(1))
+ Considered Problem:
- Strict TRS:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(X)
activate(n__g(X)) -> g(X)
f(X) -> n__f(X)
f(n__f(n__a())) -> f(n__g(f(n__a())))
g(X) -> n__g(X)
- Signature:
{a/0,activate/1,f/1,g/1} / {n__a/0,n__f/1,n__g/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {a,activate,f,g} and constructors {n__a,n__f,n__g}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
a#() -> c_1()
activate#(X) -> c_2()
activate#(n__a()) -> c_3(a#())
activate#(n__f(X)) -> c_4(f#(X))
activate#(n__g(X)) -> c_5(g#(X))
f#(X) -> c_6()
f#(n__f(n__a())) -> c_7(f#(n__g(f(n__a()))),f#(n__a()))
g#(X) -> c_8()
Weak DPs
and mark the set of starting terms.
* Step 3: UsableRules WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
a#() -> c_1()
activate#(X) -> c_2()
activate#(n__a()) -> c_3(a#())
activate#(n__f(X)) -> c_4(f#(X))
activate#(n__g(X)) -> c_5(g#(X))
f#(X) -> c_6()
f#(n__f(n__a())) -> c_7(f#(n__g(f(n__a()))),f#(n__a()))
g#(X) -> c_8()
- Weak TRS:
a() -> n__a()
activate(X) -> X
activate(n__a()) -> a()
activate(n__f(X)) -> f(X)
activate(n__g(X)) -> g(X)
f(X) -> n__f(X)
f(n__f(n__a())) -> f(n__g(f(n__a())))
g(X) -> n__g(X)
- Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {n__a/0,n__f/1,n__g/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1
,c_6/0,c_7/2,c_8/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a#,activate#,f#,g#} and constructors {n__a,n__f,n__g}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
f(X) -> n__f(X)
a#() -> c_1()
activate#(X) -> c_2()
activate#(n__a()) -> c_3(a#())
activate#(n__f(X)) -> c_4(f#(X))
activate#(n__g(X)) -> c_5(g#(X))
f#(X) -> c_6()
f#(n__f(n__a())) -> c_7(f#(n__g(f(n__a()))),f#(n__a()))
g#(X) -> c_8()
* Step 4: Trivial WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
a#() -> c_1()
activate#(X) -> c_2()
activate#(n__a()) -> c_3(a#())
activate#(n__f(X)) -> c_4(f#(X))
activate#(n__g(X)) -> c_5(g#(X))
f#(X) -> c_6()
f#(n__f(n__a())) -> c_7(f#(n__g(f(n__a()))),f#(n__a()))
g#(X) -> c_8()
- Weak TRS:
f(X) -> n__f(X)
- Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {n__a/0,n__f/1,n__g/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1
,c_6/0,c_7/2,c_8/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a#,activate#,f#,g#} and constructors {n__a,n__f,n__g}
+ Applied Processor:
Trivial
+ Details:
Consider the dependency graph
1:S:a#() -> c_1()
2:S:activate#(X) -> c_2()
3:S:activate#(n__a()) -> c_3(a#())
-->_1 a#() -> c_1():1
4:S:activate#(n__f(X)) -> c_4(f#(X))
-->_1 f#(n__f(n__a())) -> c_7(f#(n__g(f(n__a()))),f#(n__a())):7
-->_1 f#(X) -> c_6():6
5:S:activate#(n__g(X)) -> c_5(g#(X))
-->_1 g#(X) -> c_8():8
6:S:f#(X) -> c_6()
7:S:f#(n__f(n__a())) -> c_7(f#(n__g(f(n__a()))),f#(n__a()))
-->_2 f#(X) -> c_6():6
-->_1 f#(X) -> c_6():6
8:S:g#(X) -> c_8()
The dependency graph contains no loops, we remove all dependency pairs.
* Step 5: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
f(X) -> n__f(X)
- Signature:
{a/0,activate/1,f/1,g/1,a#/0,activate#/1,f#/1,g#/1} / {n__a/0,n__f/1,n__g/1,c_1/0,c_2/0,c_3/1,c_4/1,c_5/1
,c_6/0,c_7/2,c_8/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {a#,activate#,f#,g#} and constructors {n__a,n__f,n__g}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(1))