We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We add the following dependency tuples:
Strict DPs:
{ sort^#(nil()) -> c_1()
, sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y))
, insert^#(x, nil()) -> c_3()
, insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, choose^#(x, cons(v, w), y, 0()) -> c_5()
, choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
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:
{ sort^#(nil()) -> c_1()
, sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y))
, insert^#(x, nil()) -> c_3()
, insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, choose^#(x, cons(v, w), y, 0()) -> c_5()
, choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^2))
We estimate the number of application of {1,3,5} by applications of
Pre({1,3,5}) = {2,4,6,7}. Here rules are labeled as follows:
DPs:
{ 1: sort^#(nil()) -> c_1()
, 2: sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y))
, 3: insert^#(x, nil()) -> c_3()
, 4: insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, 5: choose^#(x, cons(v, w), y, 0()) -> c_5()
, 6: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, 7: choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y))
, insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
Weak DPs:
{ sort^#(nil()) -> c_1()
, insert^#(x, nil()) -> c_3()
, choose^#(x, cons(v, w), y, 0()) -> c_5() }
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
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.
{ sort^#(nil()) -> c_1()
, insert^#(x, nil()) -> c_3()
, choose^#(x, cons(v, w), y, 0()) -> c_5() }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^2)).
Strict DPs:
{ sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y))
, insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
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
{ sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) }
and lower component
{ insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
Further, following extension rules are added to the lower
component.
{ sort^#(cons(x, y)) -> sort^#(y)
, sort^#(cons(x, y)) -> insert^#(x, sort(y)) }
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:
{ sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) }
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
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: sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(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(sort) = {}, safe(nil) = {}, safe(cons) = {1, 2},
safe(insert) = {}, safe(choose) = {3, 4}, safe(0) = {},
safe(s) = {1}, safe(sort^#) = {}, safe(c_2) = {},
safe(insert^#) = {}
and precedence
sort > insert, insert > choose .
Following symbols are considered recursive:
{sort^#}
The recursion depth is 1.
Further, following argument filtering is employed:
pi(sort) = [], pi(nil) = [], pi(cons) = [2], pi(insert) = [2],
pi(choose) = [3, 4], pi(0) = [], pi(s) = [], pi(sort^#) = [1],
pi(c_2) = [1, 2], pi(insert^#) = []
Usable defined function symbols are a subset of:
{sort^#, insert^#}
For your convenience, here are the satisfied ordering constraints:
pi(sort^#(cons(x, y))) = sort^#(cons(; y);)
> c_2(insert^#(), sort^#(y;);)
= pi(c_2(insert^#(x, sort(y)), sort^#(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:
{ sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) }
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
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.
{ sort^#(cons(x, y)) -> c_2(insert^#(x, sort(y)), sort^#(y)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
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(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
Weak DPs:
{ sort^#(cons(x, y)) -> sort^#(y)
, sort^#(cons(x, y)) -> insert^#(x, sort(y)) }
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
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:
{ 2: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, 4: sort^#(cons(x, y)) -> sort^#(y)
, 5: sort^#(cons(x, y)) -> insert^#(x, sort(y)) }
Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_4) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA).
[sort](x1) = [3] x1 + [5]
[nil] = [1]
[cons](x1, x2) = [1] x1 + [1] x2 + [2]
[insert](x1, x2) = [1] x1 + [1] x2 + [5]
[choose](x1, x2, x3, x4) = [1] x1 + [1] x2 + [5]
[0] = [4]
[s](x1) = [1] x1 + [1]
[sort^#](x1) = [4] x1 + [7]
[insert^#](x1, x2) = [1] x2 + [0]
[c_4](x1) = [1] x1 + [0]
[choose^#](x1, x2, x3, x4) = [1] x2 + [0]
[c_6](x1) = [1] x1 + [1]
[c_7](x1) = [1] x1 + [0]
The order satisfies the following ordering constraints:
[sort(nil())] = [8]
> [1]
= [nil()]
[sort(cons(x, y))] = [3] x + [3] y + [11]
> [1] x + [3] y + [10]
= [insert(x, sort(y))]
[insert(x, nil())] = [1] x + [6]
> [1] x + [3]
= [cons(x, nil())]
[insert(x, cons(v, w))] = [1] x + [1] v + [1] w + [7]
>= [1] x + [1] v + [1] w + [7]
= [choose(x, cons(v, w), x, v)]
[choose(x, cons(v, w), y, 0())] = [1] x + [1] v + [1] w + [7]
> [1] x + [1] v + [1] w + [4]
= [cons(x, cons(v, w))]
[choose(x, cons(v, w), 0(), s(z))] = [1] x + [1] v + [1] w + [7]
>= [1] x + [1] v + [1] w + [7]
= [cons(v, insert(x, w))]
[choose(x, cons(v, w), s(y), s(z))] = [1] x + [1] v + [1] w + [7]
>= [1] x + [1] v + [1] w + [7]
= [choose(x, cons(v, w), y, z)]
[sort^#(cons(x, y))] = [4] x + [4] y + [15]
> [4] y + [7]
= [sort^#(y)]
[sort^#(cons(x, y))] = [4] x + [4] y + [15]
> [3] y + [5]
= [insert^#(x, sort(y))]
[insert^#(x, cons(v, w))] = [1] v + [1] w + [2]
>= [1] v + [1] w + [2]
= [c_4(choose^#(x, cons(v, w), x, v))]
[choose^#(x, cons(v, w), 0(), s(z))] = [1] v + [1] w + [2]
> [1] w + [1]
= [c_6(insert^#(x, w))]
[choose^#(x, cons(v, w), s(y), s(z))] = [1] v + [1] w + [2]
>= [1] v + [1] w + [2]
= [c_7(choose^#(x, cons(v, w), y, z))]
We return to the main proof. Consider the set of all dependency
pairs
:
{ 1: insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, 2: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, 3: choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z))
, 4: sort^#(cons(x, y)) -> sort^#(y)
, 5: sort^#(cons(x, y)) -> insert^#(x, sort(y)) }
Processor 'matrix interpretation of dimension 1' induces the
complexity certificate YES(?,O(n^1)) on application of dependency
pairs {2,4,5}. These cover all (indirect) predecessors of
dependency pairs {1,2,4,5}, their number of application is equally
bounded. The dependency pairs are shifted into the weak component.
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).
Strict DPs:
{ choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
Weak DPs:
{ sort^#(cons(x, y)) -> sort^#(y)
, sort^#(cons(x, y)) -> insert^#(x, sort(y))
, insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) }
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
Obligation:
innermost runtime complexity
Answer:
YES(O(1),O(n^1))
We use the processor 'matrix interpretation of dimension 2' to
orient following rules strictly.
DPs:
{ 1: choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z))
, 2: sort^#(cons(x, y)) -> sort^#(y)
, 3: sort^#(cons(x, y)) -> insert^#(x, sort(y))
, 4: insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, 5: choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w)) }
Trs:
{ sort(nil()) -> nil()
, insert(x, nil()) -> cons(x, nil())
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w)) }
Sub-proof:
----------
The following argument positions are usable:
Uargs(c_4) = {1}, Uargs(c_6) = {1}, Uargs(c_7) = {1}
TcT has computed the following constructor-based matrix
interpretation satisfying not(EDA) and not(IDA(1)).
[sort](x1) = [0 4] x1 + [5]
[0 2] [2]
[nil] = [0]
[0]
[cons](x1, x2) = [0 0] x1 + [0 2] x2 + [3]
[0 1] [0 1] [1]
[insert](x1, x2) = [0 4] x1 + [0 2] x2 + [5]
[0 1] [0 1] [2]
[choose](x1, x2, x3, x4) = [0 4] x1 + [0 2] x2 + [5]
[0 1] [0 1] [2]
[0] = [5]
[2]
[s](x1) = [1 0] x1 + [1]
[0 1] [4]
[sort^#](x1) = [0 6] x1 + [7]
[0 0] [5]
[insert^#](x1, x2) = [0 3] x2 + [6]
[0 0] [0]
[c_4](x1) = [1 0] x1 + [0]
[0 0] [0]
[choose^#](x1, x2, x3, x4) = [1 1] x2 + [0 2] x4 + [3]
[0 0] [0 0] [7]
[c_6](x1) = [1 1] x1 + [0]
[0 0] [0]
[c_7](x1) = [1 1] x1 + [0]
[0 0] [0]
The order satisfies the following ordering constraints:
[sort(nil())] = [5]
[2]
> [0]
[0]
= [nil()]
[sort(cons(x, y))] = [0 4] x + [0 4] y + [9]
[0 2] [0 2] [4]
>= [0 4] x + [0 4] y + [9]
[0 1] [0 2] [4]
= [insert(x, sort(y))]
[insert(x, nil())] = [0 4] x + [5]
[0 1] [2]
> [0 0] x + [3]
[0 1] [1]
= [cons(x, nil())]
[insert(x, cons(v, w))] = [0 4] x + [0 2] v + [0 2] w + [7]
[0 1] [0 1] [0 1] [3]
>= [0 4] x + [0 2] v + [0 2] w + [7]
[0 1] [0 1] [0 1] [3]
= [choose(x, cons(v, w), x, v)]
[choose(x, cons(v, w), y, 0())] = [0 4] x + [0 2] v + [0 2] w + [7]
[0 1] [0 1] [0 1] [3]
> [0 0] x + [0 2] v + [0 2] w + [5]
[0 1] [0 1] [0 1] [2]
= [cons(x, cons(v, w))]
[choose(x, cons(v, w), 0(), s(z))] = [0 4] x + [0 2] v + [0 2] w + [7]
[0 1] [0 1] [0 1] [3]
>= [0 2] x + [0 0] v + [0 2] w + [7]
[0 1] [0 1] [0 1] [3]
= [cons(v, insert(x, w))]
[choose(x, cons(v, w), s(y), s(z))] = [0 4] x + [0 2] v + [0 2] w + [7]
[0 1] [0 1] [0 1] [3]
>= [0 4] x + [0 2] v + [0 2] w + [7]
[0 1] [0 1] [0 1] [3]
= [choose(x, cons(v, w), y, z)]
[sort^#(cons(x, y))] = [0 6] x + [0 6] y + [13]
[0 0] [0 0] [5]
> [0 6] y + [7]
[0 0] [5]
= [sort^#(y)]
[sort^#(cons(x, y))] = [0 6] x + [0 6] y + [13]
[0 0] [0 0] [5]
> [0 6] y + [12]
[0 0] [0]
= [insert^#(x, sort(y))]
[insert^#(x, cons(v, w))] = [0 3] v + [0 3] w + [9]
[0 0] [0 0] [0]
> [0 3] v + [0 3] w + [7]
[0 0] [0 0] [0]
= [c_4(choose^#(x, cons(v, w), x, v))]
[choose^#(x, cons(v, w), 0(), s(z))] = [0 1] v + [0 3] w + [0 2] z + [15]
[0 0] [0 0] [0 0] [7]
> [0 3] w + [6]
[0 0] [0]
= [c_6(insert^#(x, w))]
[choose^#(x, cons(v, w), s(y), s(z))] = [0 1] v + [0 3] w + [0 2] z + [15]
[0 0] [0 0] [0 0] [7]
> [0 1] v + [0 3] w + [0 2] z + [14]
[0 0] [0 0] [0 0] [0]
= [c_7(choose^#(x, cons(v, w), y, z))]
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:
{ sort^#(cons(x, y)) -> sort^#(y)
, sort^#(cons(x, y)) -> insert^#(x, sort(y))
, insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
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.
{ sort^#(cons(x, y)) -> sort^#(y)
, sort^#(cons(x, y)) -> insert^#(x, sort(y))
, insert^#(x, cons(v, w)) -> c_4(choose^#(x, cons(v, w), x, v))
, choose^#(x, cons(v, w), 0(), s(z)) -> c_6(insert^#(x, w))
, choose^#(x, cons(v, w), s(y), s(z)) ->
c_7(choose^#(x, cons(v, w), y, z)) }
We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).
Weak Trs:
{ sort(nil()) -> nil()
, sort(cons(x, y)) -> insert(x, sort(y))
, insert(x, nil()) -> cons(x, nil())
, insert(x, cons(v, w)) -> choose(x, cons(v, w), x, v)
, choose(x, cons(v, w), y, 0()) -> cons(x, cons(v, w))
, choose(x, cons(v, w), 0(), s(z)) -> cons(v, insert(x, w))
, choose(x, cons(v, w), s(y), s(z)) ->
choose(x, cons(v, w), y, z) }
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))