We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ f(f(x)) -> f(c(f(x)))
, f(f(x)) -> f(d(f(x)))
, g(c(x)) -> x
, g(c(h(0()))) -> g(d(1()))
, g(c(1())) -> g(d(h(0())))
, g(d(x)) -> x
, g(h(x)) -> g(x) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following weak dependency pairs:
Strict DPs:
{ f^#(f(x)) -> c_1(f^#(c(f(x))))
, f^#(f(x)) -> c_2(f^#(d(f(x))))
, g^#(c(x)) -> c_3()
, g^#(c(h(0()))) -> c_4(g^#(d(1())))
, g^#(c(1())) -> c_5(g^#(d(h(0()))))
, g^#(d(x)) -> c_6()
, g^#(h(x)) -> c_7(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^#(f(x)) -> c_1(f^#(c(f(x))))
, f^#(f(x)) -> c_2(f^#(d(f(x))))
, g^#(c(x)) -> c_3()
, g^#(c(h(0()))) -> c_4(g^#(d(1())))
, g^#(c(1())) -> c_5(g^#(d(h(0()))))
, g^#(d(x)) -> c_6()
, g^#(h(x)) -> c_7(g^#(x)) }
Strict Trs:
{ f(f(x)) -> f(c(f(x)))
, f(f(x)) -> f(d(f(x)))
, g(c(x)) -> x
, g(c(h(0()))) -> g(d(1()))
, g(c(1())) -> g(d(h(0())))
, g(d(x)) -> x
, g(h(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(f(x)) -> f(c(f(x)))
, f(f(x)) -> f(d(f(x))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ f^#(f(x)) -> c_1(f^#(c(f(x))))
, f^#(f(x)) -> c_2(f^#(d(f(x))))
, g^#(c(x)) -> c_3()
, g^#(c(h(0()))) -> c_4(g^#(d(1())))
, g^#(c(1())) -> c_5(g^#(d(h(0()))))
, g^#(d(x)) -> c_6()
, g^#(h(x)) -> c_7(g^#(x)) }
Strict Trs:
{ f(f(x)) -> f(c(f(x)))
, f(f(x)) -> f(d(f(x))) }
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(c_4) = {1}, Uargs(c_5) = {1}, Uargs(c_7) = {1}
TcT has computed the following constructor-restricted matrix
interpretation.
[f](x1) = [0 2] x1 + [0]
[0 2] [1]
[c](x1) = [0]
[0]
[d](x1) = [0]
[0]
[h](x1) = [0]
[0]
[0] = [0]
[0]
[1] = [0]
[0]
[f^#](x1) = [2 0] x1 + [0]
[0 0] [0]
[c_1](x1) = [0]
[0]
[c_2](x1) = [0]
[0]
[g^#](x1) = [0]
[0]
[c_3] = [0]
[0]
[c_4](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_5](x1) = [1 0] x1 + [0]
[0 1] [0]
[c_6] = [0]
[0]
[c_7](x1) = [1 0] x1 + [0]
[0 1] [0]
The order satisfies the following ordering constraints:
[f(f(x))] = [0 4] x + [2]
[0 4] [3]
> [0]
[1]
= [f(c(f(x)))]
[f(f(x))] = [0 4] x + [2]
[0 4] [3]
> [0]
[1]
= [f(d(f(x)))]
[f^#(f(x))] = [0 4] x + [0]
[0 0] [0]
>= [0]
[0]
= [c_1(f^#(c(f(x))))]
[f^#(f(x))] = [0 4] x + [0]
[0 0] [0]
>= [0]
[0]
= [c_2(f^#(d(f(x))))]
[g^#(c(x))] = [0]
[0]
>= [0]
[0]
= [c_3()]
[g^#(c(h(0())))] = [0]
[0]
>= [0]
[0]
= [c_4(g^#(d(1())))]
[g^#(c(1()))] = [0]
[0]
>= [0]
[0]
= [c_5(g^#(d(h(0()))))]
[g^#(d(x))] = [0]
[0]
>= [0]
[0]
= [c_6()]
[g^#(h(x))] = [0]
[0]
>= [0]
[0]
= [c_7(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(n^1)).
Strict DPs:
{ f^#(f(x)) -> c_1(f^#(c(f(x))))
, f^#(f(x)) -> c_2(f^#(d(f(x))))
, g^#(c(x)) -> c_3()
, g^#(c(h(0()))) -> c_4(g^#(d(1())))
, g^#(c(1())) -> c_5(g^#(d(h(0()))))
, g^#(d(x)) -> c_6()
, g^#(h(x)) -> c_7(g^#(x)) }
Weak Trs:
{ f(f(x)) -> f(c(f(x)))
, f(f(x)) -> f(d(f(x))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Consider the dependency graph:
1: f^#(f(x)) -> c_1(f^#(c(f(x))))
2: f^#(f(x)) -> c_2(f^#(d(f(x))))
3: g^#(c(x)) -> c_3()
4: g^#(c(h(0()))) -> c_4(g^#(d(1()))) -->_1 g^#(d(x)) -> c_6() :6
5: g^#(c(1())) -> c_5(g^#(d(h(0())))) -->_1 g^#(d(x)) -> c_6() :6
6: g^#(d(x)) -> c_6()
7: g^#(h(x)) -> c_7(g^#(x))
-->_1 g^#(h(x)) -> c_7(g^#(x)) :7
-->_1 g^#(d(x)) -> c_6() :6
-->_1 g^#(c(1())) -> c_5(g^#(d(h(0())))) :5
-->_1 g^#(c(h(0()))) -> c_4(g^#(d(1()))) :4
-->_1 g^#(c(x)) -> c_3() :3
Only the nodes {3,4,6,5,7} are reachable from nodes {3,4,5,6,7}
that start derivation from marked basic terms. The nodes not
reachable are removed from the problem.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ g^#(c(x)) -> c_3()
, g^#(c(h(0()))) -> c_4(g^#(d(1())))
, g^#(c(1())) -> c_5(g^#(d(h(0()))))
, g^#(d(x)) -> c_6()
, g^#(h(x)) -> c_7(g^#(x)) }
Weak Trs:
{ f(f(x)) -> f(c(f(x)))
, f(f(x)) -> f(d(f(x))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {1,4} by applications of
Pre({1,4}) = {2,3,5}. Here rules are labeled as follows:
DPs:
{ 1: g^#(c(x)) -> c_3()
, 2: g^#(c(h(0()))) -> c_4(g^#(d(1())))
, 3: g^#(c(1())) -> c_5(g^#(d(h(0()))))
, 4: g^#(d(x)) -> c_6()
, 5: g^#(h(x)) -> c_7(g^#(x)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ g^#(c(h(0()))) -> c_4(g^#(d(1())))
, g^#(c(1())) -> c_5(g^#(d(h(0()))))
, g^#(h(x)) -> c_7(g^#(x)) }
Weak DPs:
{ g^#(c(x)) -> c_3()
, g^#(d(x)) -> c_6() }
Weak Trs:
{ f(f(x)) -> f(c(f(x)))
, f(f(x)) -> f(d(f(x))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {1,2} by applications of
Pre({1,2}) = {3}. Here rules are labeled as follows:
DPs:
{ 1: g^#(c(h(0()))) -> c_4(g^#(d(1())))
, 2: g^#(c(1())) -> c_5(g^#(d(h(0()))))
, 3: g^#(h(x)) -> c_7(g^#(x))
, 4: g^#(c(x)) -> c_3()
, 5: g^#(d(x)) -> c_6() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { g^#(h(x)) -> c_7(g^#(x)) }
Weak DPs:
{ g^#(c(x)) -> c_3()
, g^#(c(h(0()))) -> c_4(g^#(d(1())))
, g^#(c(1())) -> c_5(g^#(d(h(0()))))
, g^#(d(x)) -> c_6() }
Weak Trs:
{ f(f(x)) -> f(c(f(x)))
, f(f(x)) -> f(d(f(x))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ g^#(c(x)) -> c_3()
, g^#(c(h(0()))) -> c_4(g^#(d(1())))
, g^#(c(1())) -> c_5(g^#(d(h(0()))))
, g^#(d(x)) -> c_6() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { g^#(h(x)) -> c_7(g^#(x)) }
Weak Trs:
{ f(f(x)) -> f(c(f(x)))
, f(f(x)) -> f(d(f(x))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^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(n^1)).
Strict DPs: { g^#(h(x)) -> c_7(g^#(x)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
to orient following rules strictly.
DPs:
{ 1: g^#(h(x)) -> c_7(g^#(x)) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(h) = {1}, safe(g^#) = {}, safe(c_7) = {}
and precedence
empty .
Following symbols are considered recursive:
{g^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(h) = [1], pi(g^#) = [1], pi(c_7) = [1]
Usable defined function symbols are a subset of:
{g^#}
For your convenience, here are the satisfied ordering constraints:
pi(g^#(h(x))) = g^#(h(; x);)
> c_7(g^#(x;);)
= pi(c_7(g^#(x)))
The strictly oriented rules are moved into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak DPs: { g^#(h(x)) -> c_7(g^#(x)) }
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.
{ g^#(h(x)) -> c_7(g^#(x)) }
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))