We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict Trs:
{ minus(0(), Y) -> 0()
, minus(s(X), s(Y)) -> minus(X, Y)
, geq(X, 0()) -> true()
, geq(0(), s(Y)) -> false()
, geq(s(X), s(Y)) -> geq(X, Y)
, div(0(), s(Y)) -> 0()
, div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())
, if(true(), X, Y) -> X
, if(false(), X, Y) -> Y }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We add the following weak dependency pairs:
Strict DPs:
{ minus^#(0(), Y) -> c_1()
, minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, geq^#(X, 0()) -> c_3()
, geq^#(0(), s(Y)) -> c_4()
, geq^#(s(X), s(Y)) -> c_5(geq^#(X, Y))
, div^#(0(), s(Y)) -> c_6()
, div^#(s(X), s(Y)) ->
c_7(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))
, if^#(true(), X, Y) -> c_8()
, if^#(false(), X, Y) -> c_9() }
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:
{ minus^#(0(), Y) -> c_1()
, minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, geq^#(X, 0()) -> c_3()
, geq^#(0(), s(Y)) -> c_4()
, geq^#(s(X), s(Y)) -> c_5(geq^#(X, Y))
, div^#(0(), s(Y)) -> c_6()
, div^#(s(X), s(Y)) ->
c_7(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))
, if^#(true(), X, Y) -> c_8()
, if^#(false(), X, Y) -> c_9() }
Strict Trs:
{ minus(0(), Y) -> 0()
, minus(s(X), s(Y)) -> minus(X, Y)
, geq(X, 0()) -> true()
, geq(0(), s(Y)) -> false()
, geq(s(X), s(Y)) -> geq(X, Y)
, div(0(), s(Y)) -> 0()
, div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())
, if(true(), X, Y) -> X
, if(false(), X, Y) -> Y }
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(s) = {1}, Uargs(div) = {1}, Uargs(if) = {1, 2},
Uargs(c_2) = {1}, Uargs(c_5) = {1}, Uargs(c_7) = {1},
Uargs(if^#) = {1, 2}
TcT has computed the following constructor-restricted matrix
interpretation.
[minus](x1, x2) = [0 1] x1 + [0]
[0 0] [1]
[0] = [0]
[1]
[s](x1) = [1 0] x1 + [1]
[0 1] [2]
[geq](x1, x2) = [1 0] x1 + [1]
[0 0] [1]
[true] = [0]
[1]
[false] = [0]
[1]
[div](x1, x2) = [2 2] x1 + [0]
[2 2] [0]
[if](x1, x2, x3) = [1 1] x1 + [1 0] x2 + [1 0] x3 + [0]
[0 0] [0 1] [0 2] [0]
[minus^#](x1, x2) = [0]
[0]
[c_1] = [0]
[0]
[c_2](x1) = [1 0] x1 + [0]
[0 1] [0]
[geq^#](x1, x2) = [0]
[0]
[c_3] = [0]
[0]
[c_4] = [0]
[0]
[c_5](x1) = [1 0] x1 + [0]
[0 1] [0]
[div^#](x1, x2) = [1 2] x1 + [2 0] x2 + [0]
[0 0] [0 0] [0]
[c_6] = [0]
[0]
[c_7](x1) = [1 0] x1 + [0]
[0 1] [0]
[if^#](x1, x2, x3) = [1 1] x1 + [1 0] x2 + [0 2] x3 + [0]
[0 0] [0 0] [0 0] [0]
[c_8] = [0]
[0]
[c_9] = [0]
[0]
The order satisfies the following ordering constraints:
[minus(0(), Y)] = [1]
[1]
> [0]
[1]
= [0()]
[minus(s(X), s(Y))] = [0 1] X + [2]
[0 0] [1]
> [0 1] X + [0]
[0 0] [1]
= [minus(X, Y)]
[geq(X, 0())] = [1 0] X + [1]
[0 0] [1]
> [0]
[1]
= [true()]
[geq(0(), s(Y))] = [1]
[1]
> [0]
[1]
= [false()]
[geq(s(X), s(Y))] = [1 0] X + [2]
[0 0] [1]
> [1 0] X + [1]
[0 0] [1]
= [geq(X, Y)]
[div(0(), s(Y))] = [2]
[2]
> [0]
[1]
= [0()]
[div(s(X), s(Y))] = [2 2] X + [6]
[2 2] [6]
> [1 2] X + [5]
[0 2] [6]
= [if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())]
[if(true(), X, Y)] = [1 0] Y + [1 0] X + [1]
[0 2] [0 1] [0]
> [1 0] X + [0]
[0 1] [0]
= [X]
[if(false(), X, Y)] = [1 0] Y + [1 0] X + [1]
[0 2] [0 1] [0]
> [1 0] Y + [0]
[0 1] [0]
= [Y]
[minus^#(0(), Y)] = [0]
[0]
>= [0]
[0]
= [c_1()]
[minus^#(s(X), s(Y))] = [0]
[0]
>= [0]
[0]
= [c_2(minus^#(X, Y))]
[geq^#(X, 0())] = [0]
[0]
>= [0]
[0]
= [c_3()]
[geq^#(0(), s(Y))] = [0]
[0]
>= [0]
[0]
= [c_4()]
[geq^#(s(X), s(Y))] = [0]
[0]
>= [0]
[0]
= [c_5(geq^#(X, Y))]
[div^#(0(), s(Y))] = [2 0] Y + [4]
[0 0] [0]
> [0]
[0]
= [c_6()]
[div^#(s(X), s(Y))] = [2 0] Y + [1 2] X + [7]
[0 0] [0 0] [0]
>= [1 2] X + [7]
[0 0] [0]
= [c_7(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))]
[if^#(true(), X, Y)] = [0 2] Y + [1 0] X + [1]
[0 0] [0 0] [0]
> [0]
[0]
= [c_8()]
[if^#(false(), X, Y)] = [0 2] Y + [1 0] X + [1]
[0 0] [0 0] [0]
> [0]
[0]
= [c_9()]
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:
{ minus^#(0(), Y) -> c_1()
, minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, geq^#(X, 0()) -> c_3()
, geq^#(0(), s(Y)) -> c_4()
, geq^#(s(X), s(Y)) -> c_5(geq^#(X, Y))
, div^#(s(X), s(Y)) ->
c_7(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())) }
Weak DPs:
{ div^#(0(), s(Y)) -> c_6()
, if^#(true(), X, Y) -> c_8()
, if^#(false(), X, Y) -> c_9() }
Weak Trs:
{ minus(0(), Y) -> 0()
, minus(s(X), s(Y)) -> minus(X, Y)
, geq(X, 0()) -> true()
, geq(0(), s(Y)) -> false()
, geq(s(X), s(Y)) -> geq(X, Y)
, div(0(), s(Y)) -> 0()
, div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())
, if(true(), X, Y) -> X
, if(false(), X, Y) -> Y }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We estimate the number of application of {1,3,4,6} by applications
of Pre({1,3,4,6}) = {2,5}. Here rules are labeled as follows:
DPs:
{ 1: minus^#(0(), Y) -> c_1()
, 2: minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, 3: geq^#(X, 0()) -> c_3()
, 4: geq^#(0(), s(Y)) -> c_4()
, 5: geq^#(s(X), s(Y)) -> c_5(geq^#(X, Y))
, 6: div^#(s(X), s(Y)) ->
c_7(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))
, 7: div^#(0(), s(Y)) -> c_6()
, 8: if^#(true(), X, Y) -> c_8()
, 9: if^#(false(), X, Y) -> c_9() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, geq^#(s(X), s(Y)) -> c_5(geq^#(X, Y)) }
Weak DPs:
{ minus^#(0(), Y) -> c_1()
, geq^#(X, 0()) -> c_3()
, geq^#(0(), s(Y)) -> c_4()
, div^#(0(), s(Y)) -> c_6()
, div^#(s(X), s(Y)) ->
c_7(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))
, if^#(true(), X, Y) -> c_8()
, if^#(false(), X, Y) -> c_9() }
Weak Trs:
{ minus(0(), Y) -> 0()
, minus(s(X), s(Y)) -> minus(X, Y)
, geq(X, 0()) -> true()
, geq(0(), s(Y)) -> false()
, geq(s(X), s(Y)) -> geq(X, Y)
, div(0(), s(Y)) -> 0()
, div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())
, if(true(), X, Y) -> X
, if(false(), X, Y) -> Y }
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.
{ minus^#(0(), Y) -> c_1()
, geq^#(X, 0()) -> c_3()
, geq^#(0(), s(Y)) -> c_4()
, div^#(0(), s(Y)) -> c_6()
, div^#(s(X), s(Y)) ->
c_7(if^#(geq(X, Y), s(div(minus(X, Y), s(Y))), 0()))
, if^#(true(), X, Y) -> c_8()
, if^#(false(), X, Y) -> c_9() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, geq^#(s(X), s(Y)) -> c_5(geq^#(X, Y)) }
Weak Trs:
{ minus(0(), Y) -> 0()
, minus(s(X), s(Y)) -> minus(X, Y)
, geq(X, 0()) -> true()
, geq(0(), s(Y)) -> false()
, geq(s(X), s(Y)) -> geq(X, Y)
, div(0(), s(Y)) -> 0()
, div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0())
, if(true(), X, Y) -> X
, if(false(), X, Y) -> Y }
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:
{ minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, geq^#(s(X), s(Y)) -> c_5(geq^#(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: minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, 2: geq^#(s(X), s(Y)) -> c_5(geq^#(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(s) = {1}, safe(minus^#) = {2}, safe(c_2) = {},
safe(geq^#) = {1}, safe(c_5) = {}
and precedence
empty .
Following symbols are considered recursive:
{minus^#, geq^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(s) = [1], pi(minus^#) = [1, 2], pi(c_2) = [1], pi(geq^#) = [2],
pi(c_5) = [1]
Usable defined function symbols are a subset of:
{minus^#, geq^#}
For your convenience, here are the satisfied ordering constraints:
pi(minus^#(s(X), s(Y))) = minus^#(s(; X); s(; Y))
> c_2(minus^#(X; Y);)
= pi(c_2(minus^#(X, Y)))
pi(geq^#(s(X), s(Y))) = geq^#(s(; Y);)
> c_5(geq^#(Y;);)
= pi(c_5(geq^#(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:
{ minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, geq^#(s(X), s(Y)) -> c_5(geq^#(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.
{ minus^#(s(X), s(Y)) -> c_2(minus^#(X, Y))
, geq^#(s(X), s(Y)) -> c_5(geq^#(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^1))