We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
, log(s(0())) -> 0()
, log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We add the following dependency tuples:
Strict DPs:
{ min^#(X, 0()) -> c_1()
, min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, quot^#(0(), s(Y)) -> c_3()
, quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, log^#(s(0())) -> c_5()
, log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
and mark the set of starting terms.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ min^#(X, 0()) -> c_1()
, min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, quot^#(0(), s(Y)) -> c_3()
, quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, log^#(s(0())) -> c_5()
, log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
, log(s(0())) -> 0()
, log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We estimate the number of application of {1,3,5} by applications of
Pre({1,3,5}) = {2,4,6}. Here rules are labeled as follows:
DPs:
{ 1: min^#(X, 0()) -> c_1()
, 2: min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, 3: quot^#(0(), s(Y)) -> c_3()
, 4: quot^#(s(X), s(Y)) ->
c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, 5: log^#(s(0())) -> c_5()
, 6: log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
Weak DPs:
{ min^#(X, 0()) -> c_1()
, quot^#(0(), s(Y)) -> c_3()
, log^#(s(0())) -> c_5() }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
, log(s(0())) -> 0()
, log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
The following weak DPs constitute a sub-graph of the DG that is
closed under successors. The DPs are removed.
{ min^#(X, 0()) -> c_1()
, quot^#(0(), s(Y)) -> c_3()
, log^#(s(0())) -> c_5() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
, log(s(0())) -> 0()
, log(s(s(X))) -> s(log(s(quot(X, s(s(0())))))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^3)).
Strict DPs:
{ min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^3))
We decompose the input problem according to the dependency graph
into the upper component
{ log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
and lower component
{ min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y)) }
Further, following extension rules are added to the lower
component.
{ log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
TcT solves the upper component with certificate YES(O(1),O(n^1)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(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: log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
Trs: { min(s(X), s(Y)) -> min(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(min) = {2}, safe(0) = {}, safe(s) = {1}, safe(quot) = {},
safe(quot^#) = {}, safe(log^#) = {}, safe(c_6) = {}
and precedence
empty .
Following symbols are considered recursive:
{log^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(min) = 1, pi(0) = [], pi(s) = [1], pi(quot) = 1,
pi(quot^#) = [], pi(log^#) = [1], pi(c_6) = [1, 2]
Usable defined function symbols are a subset of:
{min, quot, quot^#, log^#}
For your convenience, here are the satisfied ordering constraints:
pi(log^#(s(s(X)))) = log^#(s(; s(; X));)
> c_6(log^#(s(; X);), quot^#();)
= pi(c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))))
pi(min(X, 0())) = X
>= X
= pi(X)
pi(min(s(X), s(Y))) = s(; X)
> X
= pi(min(X, Y))
pi(quot(0(), s(Y))) = 0()
>= 0()
= pi(0())
pi(quot(s(X), s(Y))) = s(; X)
>= s(; X)
= pi(s(quot(min(X, Y), s(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:
{ log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(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.
{ log^#(s(s(X))) ->
c_6(log^#(s(quot(X, s(s(0()))))), quot^#(X, s(s(0())))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) }
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
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y)) }
Weak DPs:
{ log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We decompose the input problem according to the dependency graph
into the upper component
{ quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
and lower component
{ min^#(s(X), s(Y)) -> c_2(min^#(X, Y)) }
Further, following extension rules are added to the lower
component.
{ quot^#(s(X), s(Y)) -> min^#(X, Y)
, quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y))
, log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
TcT solves the upper component with certificate YES(O(1),O(n^1)).
Sub-proof:
----------
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y)) }
Weak DPs:
{ log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(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: quot^#(s(X), s(Y)) ->
c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, 2: log^#(s(s(X))) -> quot^#(X, s(s(0())))
, 3: log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
Trs: { min(s(X), s(Y)) -> min(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(min) = {}, safe(0) = {}, safe(s) = {1}, safe(quot) = {},
safe(min^#) = {}, safe(quot^#) = {2}, safe(c_4) = {},
safe(log^#) = {}
and precedence
quot^# ~ log^# .
Following symbols are considered recursive:
{quot^#, log^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(min) = 1, pi(0) = [], pi(s) = [1], pi(quot) = 1, pi(min^#) = [],
pi(quot^#) = [1], pi(c_4) = [1, 2], pi(log^#) = [1]
Usable defined function symbols are a subset of:
{min, quot, min^#, quot^#, log^#}
For your convenience, here are the satisfied ordering constraints:
pi(quot^#(s(X), s(Y))) = quot^#(s(; X);)
> c_4(quot^#(X;), min^#();)
= pi(c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y)))
pi(log^#(s(s(X)))) = log^#(s(; s(; X));)
> quot^#(X;)
= pi(quot^#(X, s(s(0()))))
pi(log^#(s(s(X)))) = log^#(s(; s(; X));)
> log^#(s(; X);)
= pi(log^#(s(quot(X, s(s(0()))))))
pi(min(X, 0())) = X
>= X
= pi(X)
pi(min(s(X), s(Y))) = s(; X)
> X
= pi(min(X, Y))
pi(quot(0(), s(Y))) = 0()
>= 0()
= pi(0())
pi(quot(s(X), s(Y))) = s(; X)
>= s(; X)
= pi(s(quot(min(X, Y), s(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:
{ quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(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.
{ quot^#(s(X), s(Y)) -> c_4(quot^#(min(X, Y), s(Y)), min^#(X, Y))
, log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) }
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
We return to the main proof.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs: { min^#(s(X), s(Y)) -> c_2(min^#(X, Y)) }
Weak DPs:
{ quot^#(s(X), s(Y)) -> min^#(X, Y)
, quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y))
, log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(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: min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, 2: quot^#(s(X), s(Y)) -> min^#(X, Y)
, 3: quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y))
, 4: log^#(s(s(X))) -> quot^#(X, s(s(0())))
, 5: log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
Trs: { min(s(X), s(Y)) -> min(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(min) = {1}, safe(0) = {}, safe(s) = {1}, safe(quot) = {},
safe(min^#) = {2}, safe(c_2) = {}, safe(quot^#) = {2},
safe(log^#) = {}
and precedence
min^# ~ quot^#, quot^# ~ log^# .
Following symbols are considered recursive:
{min^#, quot^#, log^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(min) = 1, pi(0) = [], pi(s) = [1], pi(quot) = 1,
pi(min^#) = [1], pi(c_2) = [1], pi(quot^#) = [1], pi(log^#) = [1]
Usable defined function symbols are a subset of:
{min, quot, min^#, quot^#, log^#}
For your convenience, here are the satisfied ordering constraints:
pi(min^#(s(X), s(Y))) = min^#(s(; X);)
> c_2(min^#(X;);)
= pi(c_2(min^#(X, Y)))
pi(quot^#(s(X), s(Y))) = quot^#(s(; X);)
> min^#(X;)
= pi(min^#(X, Y))
pi(quot^#(s(X), s(Y))) = quot^#(s(; X);)
> quot^#(X;)
= pi(quot^#(min(X, Y), s(Y)))
pi(log^#(s(s(X)))) = log^#(s(; s(; X));)
> quot^#(X;)
= pi(quot^#(X, s(s(0()))))
pi(log^#(s(s(X)))) = log^#(s(; s(; X));)
> log^#(s(; X);)
= pi(log^#(s(quot(X, s(s(0()))))))
pi(min(X, 0())) = X
>= X
= pi(X)
pi(min(s(X), s(Y))) = s(; X)
> X
= pi(min(X, Y))
pi(quot(0(), s(Y))) = 0()
>= 0()
= pi(0())
pi(quot(s(X), s(Y))) = s(; X)
>= s(; X)
= pi(s(quot(min(X, Y), s(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:
{ min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, quot^#(s(X), s(Y)) -> min^#(X, Y)
, quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y))
, log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(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.
{ min^#(s(X), s(Y)) -> c_2(min^#(X, Y))
, quot^#(s(X), s(Y)) -> min^#(X, Y)
, quot^#(s(X), s(Y)) -> quot^#(min(X, Y), s(Y))
, log^#(s(s(X))) -> quot^#(X, s(s(0())))
, log^#(s(s(X))) -> log^#(s(quot(X, s(s(0()))))) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ min(X, 0()) -> X
, min(s(X), s(Y)) -> min(X, Y)
, quot(0(), s(Y)) -> 0()
, quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y))) }
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^3))