We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a())))
, a() -> n__a()
, g(X) -> n__g(X)
, activate(X) -> X
, activate(n__f(X)) -> f(X)
, activate(n__a()) -> a()
, activate(n__g(X)) -> g(X) }
Obligation:
runtime complexity
Answer:
YES(O(1),O(n^1))
The input is overlay and right-linear. Switching to innermost
rewriting.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a())))
, a() -> n__a()
, g(X) -> n__g(X)
, activate(X) -> X
, activate(n__f(X)) -> f(X)
, activate(n__a()) -> a()
, activate(n__g(X)) -> g(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following weak dependency pairs:
Strict DPs:
{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
, a^#() -> c_3()
, g^#(X) -> c_4()
, activate^#(X) -> c_5()
, activate^#(n__f(X)) -> c_6(f^#(X))
, activate^#(n__a()) -> c_7(a^#())
, activate^#(n__g(X)) -> c_8(g^#(X)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
, a^#() -> c_3()
, g^#(X) -> c_4()
, activate^#(X) -> c_5()
, activate^#(n__f(X)) -> c_6(f^#(X))
, activate^#(n__a()) -> c_7(a^#())
, activate^#(n__g(X)) -> c_8(g^#(X)) }
Strict Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a())))
, a() -> n__a()
, g(X) -> n__g(X)
, activate(X) -> X
, activate(n__f(X)) -> f(X)
, activate(n__a()) -> a()
, activate(n__g(X)) -> g(X) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We replace rewrite rules by usable rules:
Strict Usable Rules:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a()))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
, a^#() -> c_3()
, g^#(X) -> c_4()
, activate^#(X) -> c_5()
, activate^#(n__f(X)) -> c_6(f^#(X))
, activate^#(n__a()) -> c_7(a^#())
, activate^#(n__g(X)) -> c_8(g^#(X)) }
Strict Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The weightgap principle applies (using the following constant
growth matrix-interpretation)
The following argument positions are usable:
Uargs(f) = {1}, Uargs(n__g) = {1}, Uargs(f^#) = {1},
Uargs(c_2) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1},
Uargs(c_8) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[f](x1) = [1 2] x1 + [2]
[0 0] [1]
[n__f](x1) = [1 1] x1 + [1]
[0 0] [1]
[n__a] = [0]
[0]
[n__g](x1) = [1 0] x1 + [0]
[0 0] [0]
[f^#](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_1] = [0]
[0]
[c_2](x1) = [1 0] x1 + [0]
[0 1] [0]
[a^#] = [1]
[1]
[c_3] = [0]
[0]
[g^#](x1) = [1]
[1]
[c_4] = [0]
[0]
[activate^#](x1) = [1 0] x1 + [0]
[0 0] [0]
[c_5] = [0]
[0]
[c_6](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_7](x1) = [1 0] x1 + [1]
[0 1] [1]
[c_8](x1) = [1 0] x1 + [1]
[0 1] [1]
The order satisfies the following ordering constraints:
[f(X)] = [1 2] X + [2]
[0 0] [1]
> [1 1] X + [1]
[0 0] [1]
= [n__f(X)]
[f(n__f(n__a()))] = [5]
[1]
> [4]
[1]
= [f(n__g(f(n__a())))]
[f^#(X)] = [1 0] X + [0]
[0 0] [0]
>= [0]
[0]
= [c_1()]
[f^#(n__f(n__a()))] = [1]
[0]
? [2]
[0]
= [c_2(f^#(n__g(f(n__a()))))]
[a^#()] = [1]
[1]
> [0]
[0]
= [c_3()]
[g^#(X)] = [1]
[1]
> [0]
[0]
= [c_4()]
[activate^#(X)] = [1 0] X + [0]
[0 0] [0]
>= [0]
[0]
= [c_5()]
[activate^#(n__f(X))] = [1 1] X + [1]
[0 0] [0]
> [1 0] X + [0]
[0 0] [0]
= [c_6(f^#(X))]
[activate^#(n__a())] = [0]
[0]
? [2]
[2]
= [c_7(a^#())]
[activate^#(n__g(X))] = [1 0] X + [0]
[0 0] [0]
? [2]
[2]
= [c_8(g^#(X))]
Further, it can be verified that all rules not oriented are covered by the weightgap condition.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
, activate^#(X) -> c_5()
, activate^#(n__a()) -> c_7(a^#())
, activate^#(n__g(X)) -> c_8(g^#(X)) }
Weak DPs:
{ a^#() -> c_3()
, g^#(X) -> c_4()
, activate^#(n__f(X)) -> c_6(f^#(X)) }
Weak Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {3,4,5} by applications of
Pre({3,4,5}) = {}. Here rules are labeled as follows:
DPs:
{ 1: f^#(X) -> c_1()
, 2: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
, 3: activate^#(X) -> c_5()
, 4: activate^#(n__a()) -> c_7(a^#())
, 5: activate^#(n__g(X)) -> c_8(g^#(X))
, 6: a^#() -> c_3()
, 7: g^#(X) -> c_4()
, 8: activate^#(n__f(X)) -> c_6(f^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak DPs:
{ a^#() -> c_3()
, g^#(X) -> c_4()
, activate^#(X) -> c_5()
, activate^#(n__f(X)) -> c_6(f^#(X))
, activate^#(n__a()) -> c_7(a^#())
, activate^#(n__g(X)) -> c_8(g^#(X)) }
Weak Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ a^#() -> c_3()
, g^#(X) -> c_4()
, activate^#(X) -> c_5()
, activate^#(n__a()) -> c_7(a^#())
, activate^#(n__g(X)) -> c_8(g^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak DPs: { activate^#(n__f(X)) -> c_6(f^#(X)) }
Weak Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Consider the dependency graph
1: f^#(X) -> c_1()
2: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
-->_1 f^#(X) -> c_1() :1
3: activate^#(n__f(X)) -> c_6(f^#(X))
-->_1 f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) :2
-->_1 f^#(X) -> c_1() :1
Following roots of the dependency graph are removed, as the
considered set of starting terms is closed under reduction with
respect to these rules (modulo compound contexts).
{ activate^#(n__f(X)) -> c_6(f^#(X)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs:
{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {1} by applications of
Pre({1}) = {2}. Here rules are labeled as follows:
DPs:
{ 1: f^#(X) -> c_1()
, 2: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Strict DPs: { f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak DPs: { f^#(X) -> c_1() }
Weak Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
We estimate the number of application of {1} by applications of
Pre({1}) = {}. Here rules are labeled as follows:
DPs:
{ 1: f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a()))))
, 2: f^#(X) -> c_1() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs:
{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
Weak Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ f^#(X) -> c_1()
, f^#(n__f(n__a())) -> c_2(f^#(n__g(f(n__a())))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ f(X) -> n__f(X)
, f(n__f(n__a())) -> f(n__g(f(n__a()))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
No rule is usable, rules are removed from the input problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Rules: Empty
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(1))
Empty rules are trivially bounded
Hurray, we answered YES(O(1),O(n^1))