YES(O(1),O(n^2))
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ f(0()) -> true()
, f(1()) -> false()
, f(s(x)) -> f(x)
, if(true(), s(x), s(y)) -> s(x)
, if(false(), s(x), s(y)) -> s(y)
, g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))
, g(x, c(y)) -> c(g(x, y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add the following dependency tuples:
Strict DPs:
{ f^#(0()) -> c_1()
, f^#(1()) -> c_2()
, f^#(s(x)) -> c_3(f^#(x))
, if^#(true(), s(x), s(y)) -> c_4()
, if^#(false(), s(x), s(y)) -> c_5()
, g^#(x, c(y)) ->
c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))),
if^#(f(x), c(g(s(x), y)), c(y)),
f^#(x),
g^#(s(x), y))
, g^#(x, c(y)) -> c_7(g^#(x, y)) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ f^#(0()) -> c_1()
, f^#(1()) -> c_2()
, f^#(s(x)) -> c_3(f^#(x))
, if^#(true(), s(x), s(y)) -> c_4()
, if^#(false(), s(x), s(y)) -> c_5()
, g^#(x, c(y)) ->
c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))),
if^#(f(x), c(g(s(x), y)), c(y)),
f^#(x),
g^#(s(x), y))
, g^#(x, c(y)) -> c_7(g^#(x, y)) }
Weak Trs:
{ f(0()) -> true()
, f(1()) -> false()
, f(s(x)) -> f(x)
, if(true(), s(x), s(y)) -> s(x)
, if(false(), s(x), s(y)) -> s(y)
, g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))
, g(x, c(y)) -> c(g(x, y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We estimate the number of application of {1,2,4,5} by applications
of Pre({1,2,4,5}) = {3,6}. Here rules are labeled as follows:
DPs:
{ 1: f^#(0()) -> c_1()
, 2: f^#(1()) -> c_2()
, 3: f^#(s(x)) -> c_3(f^#(x))
, 4: if^#(true(), s(x), s(y)) -> c_4()
, 5: if^#(false(), s(x), s(y)) -> c_5()
, 6: g^#(x, c(y)) ->
c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))),
if^#(f(x), c(g(s(x), y)), c(y)),
f^#(x),
g^#(s(x), y))
, 7: g^#(x, c(y)) -> c_7(g^#(x, y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ f^#(s(x)) -> c_3(f^#(x))
, g^#(x, c(y)) ->
c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))),
if^#(f(x), c(g(s(x), y)), c(y)),
f^#(x),
g^#(s(x), y))
, g^#(x, c(y)) -> c_7(g^#(x, y)) }
Weak DPs:
{ f^#(0()) -> c_1()
, f^#(1()) -> c_2()
, if^#(true(), s(x), s(y)) -> c_4()
, if^#(false(), s(x), s(y)) -> c_5() }
Weak Trs:
{ f(0()) -> true()
, f(1()) -> false()
, f(s(x)) -> f(x)
, if(true(), s(x), s(y)) -> s(x)
, if(false(), s(x), s(y)) -> s(y)
, g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))
, g(x, c(y)) -> c(g(x, y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ f^#(0()) -> c_1()
, f^#(1()) -> c_2()
, if^#(true(), s(x), s(y)) -> c_4()
, if^#(false(), s(x), s(y)) -> c_5() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ f^#(s(x)) -> c_3(f^#(x))
, g^#(x, c(y)) ->
c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))),
if^#(f(x), c(g(s(x), y)), c(y)),
f^#(x),
g^#(s(x), y))
, g^#(x, c(y)) -> c_7(g^#(x, y)) }
Weak Trs:
{ f(0()) -> true()
, f(1()) -> false()
, f(s(x)) -> f(x)
, if(true(), s(x), s(y)) -> s(x)
, if(false(), s(x), s(y)) -> s(y)
, g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))
, g(x, c(y)) -> c(g(x, y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ g^#(x, c(y)) ->
c_6(g^#(x, if(f(x), c(g(s(x), y)), c(y))),
if^#(f(x), c(g(s(x), y)), c(y)),
f^#(x),
g^#(s(x), y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ f^#(s(x)) -> c_1(f^#(x))
, g^#(x, c(y)) -> c_2(g^#(x, y))
, g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) }
Weak Trs:
{ f(0()) -> true()
, f(1()) -> false()
, f(s(x)) -> f(x)
, if(true(), s(x), s(y)) -> s(x)
, if(false(), s(x), s(y)) -> s(y)
, g(x, c(y)) -> g(x, if(f(x), c(g(s(x), y)), c(y)))
, g(x, c(y)) -> c(g(x, y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
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^2)).
Strict DPs:
{ f^#(s(x)) -> c_1(f^#(x))
, g^#(x, c(y)) -> c_2(g^#(x, y))
, g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'polynomial interpretation' to orient
following rules strictly.
DPs:
{ 1: f^#(s(x)) -> c_1(f^#(x)) }
Sub-proof:
----------
The following argument positions are considered usable:
Uargs(c_1) = {1}, Uargs(c_2) = {1}, Uargs(c_3) = {1, 2}
TcT has computed the following constructor-restricted polynomial
interpretation.
[f](x1) = 3*x1 + 3*x1^2
[0]() = 0
[true]() = 0
[1]() = 0
[false]() = 0
[s](x1) = 1 + x1
[if](x1, x2, x3) = 3*x1 + 3*x1*x2 + 3*x1*x3 + 3*x1^2 + 3*x2 + 3*x2*x3 + 3*x2^2 + 3*x3 + 3*x3^2
[g](x1, x2) = 3*x1 + 3*x1*x2 + 3*x1^2 + 3*x2 + 3*x2^2
[c](x1) = 1 + x1
[f^#](x1) = x1
[c_1]() = 0
[c_2]() = 0
[c_3](x1) = 3*x1 + 3*x1^2
[if^#](x1, x2, x3) = 3*x1 + 3*x1*x2 + 3*x1*x3 + 3*x1^2 + 3*x2 + 3*x2*x3 + 3*x2^2 + 3*x3 + 3*x3^2
[c_4]() = 0
[c_5]() = 0
[g^#](x1, x2) = x1*x2 + x2^2
[c_6](x1, x2, x3, x4) = 3*x1 + 3*x1*x2 + 3*x1*x3 + 3*x1*x4 + 3*x1^2 + 3*x2 + 3*x2*x3 + 3*x2*x4 + 3*x2^2 + 3*x3 + 3*x3*x4 + 3*x3^2 + 3*x4 + 3*x4^2
[c_7](x1) = 3*x1 + 3*x1^2
[c]() = 0
[c_1](x1) = x1
[c_2](x1) = 1 + x1
[c_3](x1, x2) = 1 + x1 + x2
The following symbols are considered usable
{f^#, if^#, g^#}
This order satisfies the following ordering constraints.
[f^#(s(x))] = 1 + x
> x
= [c_1(f^#(x))]
[g^#(x, c(y))] = x + x*y + 1 + 2*y + y^2
>= 1 + x*y + y^2
= [c_2(g^#(x, y))]
[g^#(x, c(y))] = x + x*y + 1 + 2*y + y^2
>= 1 + x + y + x*y + y^2
= [c_3(f^#(x), g^#(s(x), y))]
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(n^1)).
Strict DPs:
{ g^#(x, c(y)) -> c_2(g^#(x, y))
, g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) }
Weak DPs: { f^#(s(x)) -> c_1(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.
{ f^#(s(x)) -> c_1(f^#(x)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ g^#(x, c(y)) -> c_2(g^#(x, y))
, g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
Due to missing edges in the dependency-graph, the right-hand sides
of following rules could be simplified:
{ g^#(x, c(y)) -> c_3(f^#(x), g^#(s(x), y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ g^#(x, c(y)) -> c_1(g^#(x, y))
, g^#(x, c(y)) -> c_2(g^#(s(x), y)) }
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^#(x, c(y)) -> c_1(g^#(x, y))
, 2: g^#(x, c(y)) -> c_2(g^#(s(x), y)) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(f) = {}, safe(0) = {}, safe(true) = {}, safe(1) = {},
safe(false) = {}, safe(s) = {1}, safe(if) = {}, safe(g) = {},
safe(c) = {1}, safe(f^#) = {}, safe(c_1) = {}, safe(c_2) = {},
safe(c_3) = {}, safe(if^#) = {}, safe(c_4) = {}, safe(c_5) = {},
safe(g^#) = {1}, safe(c_6) = {}, safe(c_7) = {}, safe(c) = {},
safe(c_1) = {}, safe(c_2) = {}, safe(c_3) = {}, safe(c) = {},
safe(c_1) = {}, safe(c_2) = {}
and precedence
empty .
Following symbols are considered recursive:
{g^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(f) = [], pi(0) = [], pi(true) = [], pi(1) = [], pi(false) = [],
pi(s) = 1, pi(if) = [], pi(g) = [], pi(c) = [1], pi(f^#) = [],
pi(c_1) = [], pi(c_2) = [], pi(c_3) = [], pi(if^#) = [],
pi(c_4) = [], pi(c_5) = [], pi(g^#) = [1, 2], pi(c_6) = [],
pi(c_7) = [], pi(c) = [], pi(c_1) = [], pi(c_2) = [], pi(c_3) = [],
pi(c) = [], pi(c_1) = [1], pi(c_2) = [1]
Usable defined function symbols are a subset of:
{f^#, if^#, g^#}
For your convenience, here are the satisfied ordering constraints:
pi(g^#(x, c(y))) = g^#(c(; y); x)
> c_1(g^#(y; x);)
= pi(c_1(g^#(x, y)))
pi(g^#(x, c(y))) = g^#(c(; y); x)
> c_2(g^#(y; x);)
= pi(c_2(g^#(s(x), y)))
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^#(x, c(y)) -> c_1(g^#(x, y))
, g^#(x, c(y)) -> c_2(g^#(s(x), y)) }
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^#(x, c(y)) -> c_1(g^#(x, y))
, g^#(x, c(y)) -> c_2(g^#(s(x), y)) }
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^2))