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