We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
, isort(Nil(), r) -> r
, inssort(xs) -> isort(xs, Nil()) }
Weak Trs:
{ insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add the following dependency tuples:
Strict DPs:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
<^#(x', x))
, insert^#(x, Nil()) -> c_2()
, isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r))
, isort^#(Nil(), r) -> c_4()
, inssort^#(xs) -> c_5(isort^#(xs, Nil())) }
Weak DPs:
{ insert[Ite][False][Ite]^#(True(), x, r) -> c_6()
, insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_7(insert^#(x', xs))
, <^#(x, 0()) -> c_8()
, <^#(S(x), S(y)) -> c_9(<^#(x, y))
, <^#(0(), S(y)) -> c_10() }
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:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
<^#(x', x))
, insert^#(x, Nil()) -> c_2()
, isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r))
, isort^#(Nil(), r) -> c_4()
, inssort^#(xs) -> c_5(isort^#(xs, Nil())) }
Weak DPs:
{ insert[Ite][False][Ite]^#(True(), x, r) -> c_6()
, insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_7(insert^#(x', xs))
, <^#(x, 0()) -> c_8()
, <^#(S(x), S(y)) -> c_9(<^#(x, y))
, <^#(0(), S(y)) -> c_10() }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True()
, isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
, isort(Nil(), r) -> r
, inssort(xs) -> isort(xs, Nil()) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We estimate the number of application of {4} by applications of
Pre({4}) = {3,5}. Here rules are labeled as follows:
DPs:
{ 1: insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
<^#(x', x))
, 2: insert^#(x, Nil()) -> c_2()
, 3: isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r))
, 4: isort^#(Nil(), r) -> c_4()
, 5: inssort^#(xs) -> c_5(isort^#(xs, Nil()))
, 6: insert[Ite][False][Ite]^#(True(), x, r) -> c_6()
, 7: insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_7(insert^#(x', xs))
, 8: <^#(x, 0()) -> c_8()
, 9: <^#(S(x), S(y)) -> c_9(<^#(x, y))
, 10: <^#(0(), S(y)) -> c_10() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
<^#(x', x))
, insert^#(x, Nil()) -> c_2()
, isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r))
, inssort^#(xs) -> c_5(isort^#(xs, Nil())) }
Weak DPs:
{ insert[Ite][False][Ite]^#(True(), x, r) -> c_6()
, insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_7(insert^#(x', xs))
, <^#(x, 0()) -> c_8()
, <^#(S(x), S(y)) -> c_9(<^#(x, y))
, <^#(0(), S(y)) -> c_10()
, isort^#(Nil(), r) -> c_4() }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True()
, isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
, isort(Nil(), r) -> r
, inssort(xs) -> isort(xs, Nil()) }
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.
{ insert[Ite][False][Ite]^#(True(), x, r) -> c_6()
, <^#(x, 0()) -> c_8()
, <^#(S(x), S(y)) -> c_9(<^#(x, y))
, <^#(0(), S(y)) -> c_10()
, isort^#(Nil(), r) -> c_4() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
<^#(x', x))
, insert^#(x, Nil()) -> c_2()
, isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r))
, inssort^#(xs) -> c_5(isort^#(xs, Nil())) }
Weak DPs:
{ insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_7(insert^#(x', xs)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True()
, isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
, isort(Nil(), r) -> r
, inssort(xs) -> isort(xs, Nil()) }
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:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)),
<^#(x', x)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
, insert^#(x, Nil()) -> c_2()
, isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r))
, inssort^#(xs) -> c_4(isort^#(xs, Nil())) }
Weak DPs:
{ insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True()
, isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
, isort(Nil(), r) -> r
, inssort(xs) -> isort(xs, Nil()) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We replace rewrite rules by usable rules:
Weak Usable Rules:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
, insert^#(x, Nil()) -> c_2()
, isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r))
, inssort^#(xs) -> c_4(isort^#(xs, Nil())) }
Weak DPs:
{ insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
Consider the dependency graph
1: insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
-->_1 insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs)) :5
2: insert^#(x, Nil()) -> c_2()
3: isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r))
-->_1 isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) :3
-->_2 insert^#(x, Nil()) -> c_2() :2
-->_2 insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) :1
4: inssort^#(xs) -> c_4(isort^#(xs, Nil()))
-->_1 isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) :3
5: insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs))
-->_1 insert^#(x, Nil()) -> c_2() :2
-->_1 insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) :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).
{ inssort^#(xs) -> c_4(isort^#(xs, Nil())) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
, insert^#(x, Nil()) -> c_2()
, isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) }
Weak DPs:
{ insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 2: insert^#(x, Nil()) -> c_2()
, 3: isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) }
Trs:
{ insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_3) = {1, 2}, Uargs(c_5) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[insert](x1, x2) = [4] x2 + [3]
[True] = [0]
[insert[Ite][False][Ite]](x1, x2, x3) = [2] x1 + [4] x3 + [3]
[<](x1, x2) = [0]
[S](x1) = [1] x1 + [0]
[Cons](x1, x2) = [1] x2 + [3]
[Nil] = [1]
[0] = [6]
[False] = [0]
[insert^#](x1, x2) = [2]
[insert[Ite][False][Ite]^#](x1, x2, x3) = [6] x1 + [2]
[isort^#](x1, x2) = [3] x1 + [0]
[c_1](x1) = [1] x1 + [0]
[c_2] = [0]
[c_3](x1, x2) = [1] x1 + [2] x2 + [0]
[c_5](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[insert(x', Cons(x, xs))] = [4] xs + [15]
>= [4] xs + [15]
= [insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))]
[insert(x, Nil())] = [7]
> [4]
= [Cons(x, Nil())]
[insert[Ite][False][Ite](True(), x, r)] = [4] r + [3]
>= [1] r + [3]
= [Cons(x, r)]
[insert[Ite][False][Ite](False(), x', Cons(x, xs))] = [4] xs + [15]
> [4] xs + [6]
= [Cons(x, insert(x', xs))]
[<(x, 0())] = [0]
>= [0]
= [False()]
[<(S(x), S(y))] = [0]
>= [0]
= [<(x, y)]
[<(0(), S(y))] = [0]
>= [0]
= [True()]
[insert^#(x', Cons(x, xs))] = [2]
>= [2]
= [c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))]
[insert^#(x, Nil())] = [2]
> [0]
= [c_2()]
[insert[Ite][False][Ite]^#(False(), x', Cons(x, xs))] = [2]
>= [2]
= [c_5(insert^#(x', xs))]
[isort^#(Cons(x, xs), r)] = [3] xs + [9]
> [3] xs + [4]
= [c_3(isort^#(xs, insert(x, r)), insert^#(x, r))]
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^2)).
Strict DPs:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) }
Weak DPs:
{ insert^#(x, Nil()) -> c_2()
, insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs))
, isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
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.
{ insert^#(x, Nil()) -> c_2() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) }
Weak DPs:
{ insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs))
, isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
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
{ isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) }
and lower component
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
, insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs)) }
Further, following extension rules are added to the lower
component.
{ isort^#(Cons(x, xs), r) -> insert^#(x, r)
, isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
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:
{ isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
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: isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) }
Sub-proof:
----------
The input was oriented with the instance of 'Small Polynomial Path
Order (PS,1-bounded)' as induced by the safe mapping
safe(insert) = {}, safe(True) = {},
safe(insert[Ite][False][Ite]) = {3}, safe(<) = {1, 2},
safe(S) = {1}, safe(Cons) = {1, 2}, safe(Nil) = {}, safe(0) = {},
safe(False) = {}, safe(insert^#) = {}, safe(isort^#) = {2},
safe(c_3) = {}
and precedence
insert > insert[Ite][False][Ite] .
Following symbols are considered recursive:
{isort^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(insert) = [], pi(True) = [],
pi(insert[Ite][False][Ite]) = [1, 3], pi(<) = [1, 2],
pi(S) = [], pi(Cons) = [2], pi(Nil) = [], pi(0) = [],
pi(False) = [], pi(insert^#) = [], pi(isort^#) = [1],
pi(c_3) = [1, 2]
Usable defined function symbols are a subset of:
{insert^#, isort^#}
For your convenience, here are the satisfied ordering constraints:
pi(isort^#(Cons(x, xs), r)) = isort^#(Cons(; xs);)
> c_3(isort^#(xs;), insert^#();)
= pi(c_3(isort^#(xs, insert(x, r)), insert^#(x, r)))
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:
{ isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
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.
{ isort^#(Cons(x, xs), r) ->
c_3(isort^#(xs, insert(x, r)), insert^#(x, r)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
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:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs))) }
Weak DPs:
{ insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs))
, isort^#(Cons(x, xs), r) -> insert^#(x, r)
, isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 1' to
orient following rules strictly.
DPs:
{ 1: insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
, 2: insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs))
, 3: isort^#(Cons(x, xs), r) -> insert^#(x, r)
, 4: isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
Trs:
{ insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_1) = {1}, Uargs(c_5) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[insert](x1, x2) = [1] x2 + [4]
[True] = [0]
[insert[Ite][False][Ite]](x1, x2, x3) = [1] x3 + [4]
[<](x1, x2) = [0]
[S](x1) = [1] x1 + [0]
[Cons](x1, x2) = [1] x2 + [3]
[Nil] = [0]
[0] = [1]
[False] = [0]
[insert^#](x1, x2) = [1] x2 + [4]
[insert[Ite][False][Ite]^#](x1, x2, x3) = [4] x1 + [1] x3 + [3]
[isort^#](x1, x2) = [3] x1 + [2] x2 + [6]
[c_1](x1) = [1] x1 + [0]
[c_5](x1) = [1] x1 + [1]
The order satisfies the following ordering constraints:
[insert(x', Cons(x, xs))] = [1] xs + [7]
>= [1] xs + [7]
= [insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))]
[insert(x, Nil())] = [4]
> [3]
= [Cons(x, Nil())]
[insert[Ite][False][Ite](True(), x, r)] = [1] r + [4]
> [1] r + [3]
= [Cons(x, r)]
[insert[Ite][False][Ite](False(), x', Cons(x, xs))] = [1] xs + [7]
>= [1] xs + [7]
= [Cons(x, insert(x', xs))]
[<(x, 0())] = [0]
>= [0]
= [False()]
[<(S(x), S(y))] = [0]
>= [0]
= [<(x, y)]
[<(0(), S(y))] = [0]
>= [0]
= [True()]
[insert^#(x', Cons(x, xs))] = [1] xs + [7]
> [1] xs + [6]
= [c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))]
[insert[Ite][False][Ite]^#(False(), x', Cons(x, xs))] = [1] xs + [6]
> [1] xs + [5]
= [c_5(insert^#(x', xs))]
[isort^#(Cons(x, xs), r)] = [3] xs + [2] r + [15]
> [1] r + [4]
= [insert^#(x, r)]
[isort^#(Cons(x, xs), r)] = [3] xs + [2] r + [15]
> [3] xs + [2] r + [14]
= [isort^#(xs, insert(x, r))]
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:
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
, insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs))
, isort^#(Cons(x, xs), r) -> insert^#(x, r)
, isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
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.
{ insert^#(x', Cons(x, xs)) ->
c_1(insert[Ite][False][Ite]^#(<(x', x), x', Cons(x, xs)))
, insert[Ite][False][Ite]^#(False(), x', Cons(x, xs)) ->
c_5(insert^#(x', xs))
, isort^#(Cons(x, xs), r) -> insert^#(x, r)
, isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ insert(x', Cons(x, xs)) ->
insert[Ite][False][Ite](<(x', x), x', Cons(x, xs))
, insert(x, Nil()) -> Cons(x, Nil())
, insert[Ite][False][Ite](True(), x, r) -> Cons(x, r)
, insert[Ite][False][Ite](False(), x', Cons(x, xs)) ->
Cons(x, insert(x', xs))
, <(x, 0()) -> False()
, <(S(x), S(y)) -> <(x, y)
, <(0(), S(y)) -> True() }
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^2))