YES(O(1),O(n^2))
556.26/148.03 YES(O(1),O(n^2))
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(n^2)).
556.26/148.03
556.26/148.03 Strict Trs:
556.26/148.03 { insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
556.26/148.03 , isort(Nil(), r) -> Nil()
556.26/148.03 , inssort(xs) -> isort(xs, Nil()) }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(n^2))
556.26/148.03
556.26/148.03 We add the following dependency tuples:
556.26/148.03
556.26/148.03 Strict DPs:
556.26/148.03 { insert^#(S(x), r) ->
556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x))
556.26/148.03 , isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r))
556.26/148.03 , isort^#(Nil(), r) -> c_3()
556.26/148.03 , inssort^#(xs) -> c_4(isort^#(xs, Nil())) }
556.26/148.03 Weak DPs:
556.26/148.03 { insert[Ite]^#(True(), x, r) -> c_5()
556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_6(insert^#(x', xs))
556.26/148.03 , <^#(x, 0()) -> c_7()
556.26/148.03 , <^#(S(x), S(y)) -> c_8(<^#(x, y))
556.26/148.03 , <^#(0(), S(y)) -> c_9() }
556.26/148.03
556.26/148.03 and mark the set of starting terms.
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(n^2)).
556.26/148.03
556.26/148.03 Strict DPs:
556.26/148.03 { insert^#(S(x), r) ->
556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x))
556.26/148.03 , isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r))
556.26/148.03 , isort^#(Nil(), r) -> c_3()
556.26/148.03 , inssort^#(xs) -> c_4(isort^#(xs, Nil())) }
556.26/148.03 Weak DPs:
556.26/148.03 { insert[Ite]^#(True(), x, r) -> c_5()
556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_6(insert^#(x', xs))
556.26/148.03 , <^#(x, 0()) -> c_7()
556.26/148.03 , <^#(S(x), S(y)) -> c_8(<^#(x, y))
556.26/148.03 , <^#(0(), S(y)) -> c_9() }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True()
556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
556.26/148.03 , isort(Nil(), r) -> Nil()
556.26/148.03 , inssort(xs) -> isort(xs, Nil()) }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(n^2))
556.26/148.03
556.26/148.03 We estimate the number of application of {3} by applications of
556.26/148.03 Pre({3}) = {2,4}. Here rules are labeled as follows:
556.26/148.03
556.26/148.03 DPs:
556.26/148.03 { 1: insert^#(S(x), r) ->
556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x))
556.26/148.03 , 2: isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r))
556.26/148.03 , 3: isort^#(Nil(), r) -> c_3()
556.26/148.03 , 4: inssort^#(xs) -> c_4(isort^#(xs, Nil()))
556.26/148.03 , 5: insert[Ite]^#(True(), x, r) -> c_5()
556.26/148.03 , 6: insert[Ite]^#(False(), x', Cons(x, xs)) ->
556.26/148.03 c_6(insert^#(x', xs))
556.26/148.03 , 7: <^#(x, 0()) -> c_7()
556.26/148.03 , 8: <^#(S(x), S(y)) -> c_8(<^#(x, y))
556.26/148.03 , 9: <^#(0(), S(y)) -> c_9() }
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(n^2)).
556.26/148.03
556.26/148.03 Strict DPs:
556.26/148.03 { insert^#(S(x), r) ->
556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x))
556.26/148.03 , isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r))
556.26/148.03 , inssort^#(xs) -> c_4(isort^#(xs, Nil())) }
556.26/148.03 Weak DPs:
556.26/148.03 { insert[Ite]^#(True(), x, r) -> c_5()
556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_6(insert^#(x', xs))
556.26/148.03 , <^#(x, 0()) -> c_7()
556.26/148.03 , <^#(S(x), S(y)) -> c_8(<^#(x, y))
556.26/148.03 , <^#(0(), S(y)) -> c_9()
556.26/148.03 , isort^#(Nil(), r) -> c_3() }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True()
556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
556.26/148.03 , isort(Nil(), r) -> Nil()
556.26/148.03 , inssort(xs) -> isort(xs, Nil()) }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(n^2))
556.26/148.03
556.26/148.03 The following weak DPs constitute a sub-graph of the DG that is
556.26/148.03 closed under successors. The DPs are removed.
556.26/148.03
556.26/148.03 { insert[Ite]^#(True(), x, r) -> c_5()
556.26/148.03 , <^#(x, 0()) -> c_7()
556.26/148.03 , <^#(S(x), S(y)) -> c_8(<^#(x, y))
556.26/148.03 , <^#(0(), S(y)) -> c_9()
556.26/148.03 , isort^#(Nil(), r) -> c_3() }
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(n^2)).
556.26/148.03
556.26/148.03 Strict DPs:
556.26/148.03 { insert^#(S(x), r) ->
556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x))
556.26/148.03 , isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r))
556.26/148.03 , inssort^#(xs) -> c_4(isort^#(xs, Nil())) }
556.26/148.03 Weak DPs:
556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) ->
556.26/148.03 c_6(insert^#(x', xs)) }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True()
556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
556.26/148.03 , isort(Nil(), r) -> Nil()
556.26/148.03 , inssort(xs) -> isort(xs, Nil()) }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(n^2))
556.26/148.03
556.26/148.03 Due to missing edges in the dependency-graph, the right-hand sides
556.26/148.03 of following rules could be simplified:
556.26/148.03
556.26/148.03 { insert^#(S(x), r) ->
556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r), <^#(S(x), x)) }
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(n^2)).
556.26/148.03
556.26/148.03 Strict DPs:
556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r))
556.26/148.03 , isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r))
556.26/148.03 , inssort^#(xs) -> c_3(isort^#(xs, Nil())) }
556.26/148.03 Weak DPs:
556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) ->
556.26/148.03 c_4(insert^#(x', xs)) }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True()
556.26/148.03 , isort(Cons(x, xs), r) -> isort(xs, insert(x, r))
556.26/148.03 , isort(Nil(), r) -> Nil()
556.26/148.03 , inssort(xs) -> isort(xs, Nil()) }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(n^2))
556.26/148.03
556.26/148.03 We replace rewrite rules by usable rules:
556.26/148.03
556.26/148.03 Weak Usable Rules:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(n^2)).
556.26/148.03
556.26/148.03 Strict DPs:
556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r))
556.26/148.03 , isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r))
556.26/148.03 , inssort^#(xs) -> c_3(isort^#(xs, Nil())) }
556.26/148.03 Weak DPs:
556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) ->
556.26/148.03 c_4(insert^#(x', xs)) }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(n^2))
556.26/148.03
556.26/148.03 Consider the dependency graph
556.26/148.03
556.26/148.03 1: insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r))
556.26/148.03 -->_1 insert[Ite]^#(False(), x', Cons(x, xs)) ->
556.26/148.03 c_4(insert^#(x', xs)) :4
556.26/148.03
556.26/148.03 2: isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r))
556.26/148.03 -->_1 isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) :2
556.26/148.03 -->_2 insert^#(S(x), r) ->
556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r)) :1
556.26/148.03
556.26/148.03 3: inssort^#(xs) -> c_3(isort^#(xs, Nil()))
556.26/148.03 -->_1 isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) :2
556.26/148.03
556.26/148.03 4: insert[Ite]^#(False(), x', Cons(x, xs)) -> c_4(insert^#(x', xs))
556.26/148.03 -->_1 insert^#(S(x), r) ->
556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r)) :1
556.26/148.03
556.26/148.03
556.26/148.03 Following roots of the dependency graph are removed, as the
556.26/148.03 considered set of starting terms is closed under reduction with
556.26/148.03 respect to these rules (modulo compound contexts).
556.26/148.03
556.26/148.03 { inssort^#(xs) -> c_3(isort^#(xs, Nil())) }
556.26/148.03
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(n^2)).
556.26/148.03
556.26/148.03 Strict DPs:
556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r))
556.26/148.03 , isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) }
556.26/148.03 Weak DPs:
556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) ->
556.26/148.03 c_4(insert^#(x', xs)) }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(n^2))
556.26/148.03
556.26/148.03 We decompose the input problem according to the dependency graph
556.26/148.03 into the upper component
556.26/148.03
556.26/148.03 { isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) }
556.26/148.03
556.26/148.03 and lower component
556.26/148.03
556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r))
556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) ->
556.26/148.03 c_4(insert^#(x', xs)) }
556.26/148.03
556.26/148.03 Further, following extension rules are added to the lower
556.26/148.03 component.
556.26/148.03
556.26/148.03 { isort^#(Cons(x, xs), r) -> insert^#(x, r)
556.26/148.03 , isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
556.26/148.03
556.26/148.03 TcT solves the upper component with certificate YES(O(1),O(n^1)).
556.26/148.03
556.26/148.03 Sub-proof:
556.26/148.03 ----------
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(n^1)).
556.26/148.03
556.26/148.03 Strict DPs:
556.26/148.03 { isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(n^1))
556.26/148.03
556.26/148.03 We use the processor 'Small Polynomial Path Order (PS,1-bounded)'
556.26/148.03 to orient following rules strictly.
556.26/148.03
556.26/148.03 DPs:
556.26/148.03 { 1: isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) }
556.26/148.03 Trs:
556.26/148.03 { <(x, 0()) -> False()
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03
556.26/148.03 Sub-proof:
556.26/148.03 ----------
556.26/148.03 The input was oriented with the instance of 'Small Polynomial Path
556.26/148.03 Order (PS,1-bounded)' as induced by the safe mapping
556.26/148.03
556.26/148.03 safe(insert[Ite]) = {1}, safe(insert) = {}, safe(True) = {},
556.26/148.03 safe(S) = {1}, safe(<) = {}, safe(Cons) = {1, 2}, safe(0) = {},
556.26/148.03 safe(False) = {}, safe(insert^#) = {}, safe(isort^#) = {2},
556.26/148.03 safe(c_2) = {}
556.26/148.03
556.26/148.03 and precedence
556.26/148.03
556.26/148.03 insert[Ite] > insert, insert[Ite] > <, insert > <,
556.26/148.03 isort^# > insert, isort^# > < .
556.26/148.03
556.26/148.03 Following symbols are considered recursive:
556.26/148.03
556.26/148.03 {insert[Ite], isort^#}
556.26/148.03
556.26/148.03 The recursion depth is 1.
556.26/148.03
556.26/148.03 Further, following argument filtering is employed:
556.26/148.03
556.26/148.03 pi(insert[Ite]) = [1], pi(insert) = [1, 2], pi(True) = [],
556.26/148.03 pi(S) = [], pi(<) = [1, 2], pi(Cons) = [1, 2], pi(0) = [],
556.26/148.03 pi(False) = [], pi(insert^#) = [1], pi(isort^#) = [1],
556.26/148.03 pi(c_2) = [1, 2]
556.26/148.03
556.26/148.03 Usable defined function symbols are a subset of:
556.26/148.03
556.26/148.03 {insert^#, isort^#}
556.26/148.03
556.26/148.03 For your convenience, here are the satisfied ordering constraints:
556.26/148.03
556.26/148.03 pi(isort^#(Cons(x, xs), r)) = isort^#(Cons(; x, xs);)
556.26/148.03 > c_2(isort^#(xs;), insert^#(x;);)
556.26/148.03 = pi(c_2(isort^#(xs, insert(x, r)), insert^#(x, r)))
556.26/148.03
556.26/148.03
556.26/148.03 The strictly oriented rules are moved into the weak component.
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(1)).
556.26/148.03
556.26/148.03 Weak DPs:
556.26/148.03 { isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(1))
556.26/148.03
556.26/148.03 The following weak DPs constitute a sub-graph of the DG that is
556.26/148.03 closed under successors. The DPs are removed.
556.26/148.03
556.26/148.03 { isort^#(Cons(x, xs), r) ->
556.26/148.03 c_2(isort^#(xs, insert(x, r)), insert^#(x, r)) }
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(1)).
556.26/148.03
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(1))
556.26/148.03
556.26/148.03 No rule is usable, rules are removed from the input problem.
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(1)).
556.26/148.03
556.26/148.03 Rules: Empty
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(1))
556.26/148.03
556.26/148.03 Empty rules are trivially bounded
556.26/148.03
556.26/148.03 We return to the main proof.
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(n^1)).
556.26/148.03
556.26/148.03 Strict DPs:
556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r)) }
556.26/148.03 Weak DPs:
556.26/148.03 { insert[Ite]^#(False(), x', Cons(x, xs)) -> c_4(insert^#(x', xs))
556.26/148.03 , isort^#(Cons(x, xs), r) -> insert^#(x, r)
556.26/148.03 , isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(n^1))
556.26/148.03
556.26/148.03 We use the processor 'matrix interpretation of dimension 1' to
556.26/148.03 orient following rules strictly.
556.26/148.03
556.26/148.03 DPs:
556.26/148.03 { 2: insert[Ite]^#(False(), x', Cons(x, xs)) ->
556.26/148.03 c_4(insert^#(x', xs))
556.26/148.03 , 3: isort^#(Cons(x, xs), r) -> insert^#(x, r) }
556.26/148.03
556.26/148.03 Sub-proof:
556.26/148.03 ----------
556.26/148.03 The following argument positions are usable:
556.26/148.03 Uargs(c_1) = {1}, Uargs(c_4) = {1}
556.26/148.03
556.26/148.03 TcT has computed the following constructor-based matrix
556.26/148.03 interpretation satisfying not(EDA).
556.26/148.03
556.26/148.03 [insert[Ite]](x1, x2, x3) = [4] x2 + [1] x3 + [4]
556.26/148.03
556.26/148.03 [insert](x1, x2) = [1] x2 + [4]
556.26/148.03
556.26/148.03 [True] = [0]
556.26/148.03
556.26/148.03 [S](x1) = [0]
556.26/148.03
556.26/148.03 [<](x1, x2) = [0]
556.26/148.03
556.26/148.03 [Cons](x1, x2) = [1] x2 + [4]
556.26/148.03
556.26/148.03 [0] = [0]
556.26/148.03
556.26/148.03 [False] = [0]
556.26/148.03
556.26/148.03 [insert^#](x1, x2) = [2] x2 + [0]
556.26/148.03
556.26/148.03 [insert[Ite]^#](x1, x2, x3) = [2] x3 + [0]
556.26/148.03
556.26/148.03 [isort^#](x1, x2) = [2] x1 + [2] x2 + [0]
556.26/148.03
556.26/148.03 [c_1](x1) = [1] x1 + [0]
556.26/148.03
556.26/148.03 [c_4](x1) = [1] x1 + [1]
556.26/148.03
556.26/148.03 The order satisfies the following ordering constraints:
556.26/148.03
556.26/148.03 [insert[Ite](True(), x, r)] = [4] x + [1] r + [4]
556.26/148.03 >= [1] r + [4]
556.26/148.03 = [Cons(x, r)]
556.26/148.03
556.26/148.03 [insert[Ite](False(), x', Cons(x, xs))] = [1] xs + [4] x' + [8]
556.26/148.03 >= [1] xs + [8]
556.26/148.03 = [Cons(x, insert(x', xs))]
556.26/148.03
556.26/148.03 [insert(S(x), r)] = [1] r + [4]
556.26/148.03 >= [1] r + [4]
556.26/148.03 = [insert[Ite](<(S(x), x), S(x), r)]
556.26/148.03
556.26/148.03 [<(x, 0())] = [0]
556.26/148.03 >= [0]
556.26/148.03 = [False()]
556.26/148.03
556.26/148.03 [<(S(x), S(y))] = [0]
556.26/148.03 >= [0]
556.26/148.03 = [<(x, y)]
556.26/148.03
556.26/148.03 [<(0(), S(y))] = [0]
556.26/148.03 >= [0]
556.26/148.03 = [True()]
556.26/148.03
556.26/148.03 [insert^#(S(x), r)] = [2] r + [0]
556.26/148.03 >= [2] r + [0]
556.26/148.03 = [c_1(insert[Ite]^#(<(S(x), x), S(x), r))]
556.26/148.03
556.26/148.03 [insert[Ite]^#(False(), x', Cons(x, xs))] = [2] xs + [8]
556.26/148.03 > [2] xs + [1]
556.26/148.03 = [c_4(insert^#(x', xs))]
556.26/148.03
556.26/148.03 [isort^#(Cons(x, xs), r)] = [2] xs + [2] r + [8]
556.26/148.03 > [2] r + [0]
556.26/148.03 = [insert^#(x, r)]
556.26/148.03
556.26/148.03 [isort^#(Cons(x, xs), r)] = [2] xs + [2] r + [8]
556.26/148.03 >= [2] xs + [2] r + [8]
556.26/148.03 = [isort^#(xs, insert(x, r))]
556.26/148.03
556.26/148.03
556.26/148.03 We return to the main proof. Consider the set of all dependency
556.26/148.03 pairs
556.26/148.03
556.26/148.03 :
556.26/148.03 { 1: insert^#(S(x), r) ->
556.26/148.03 c_1(insert[Ite]^#(<(S(x), x), S(x), r))
556.26/148.03 , 2: insert[Ite]^#(False(), x', Cons(x, xs)) ->
556.26/148.03 c_4(insert^#(x', xs))
556.26/148.03 , 3: isort^#(Cons(x, xs), r) -> insert^#(x, r)
556.26/148.03 , 4: isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
556.26/148.03
556.26/148.03 Processor 'matrix interpretation of dimension 1' induces the
556.26/148.03 complexity certificate YES(?,O(n^1)) on application of dependency
556.26/148.03 pairs {2,3}. These cover all (indirect) predecessors of dependency
556.26/148.03 pairs {1,2,3}, their number of application is equally bounded. The
556.26/148.03 dependency pairs are shifted into the weak component.
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(1)).
556.26/148.03
556.26/148.03 Weak DPs:
556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r))
556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_4(insert^#(x', xs))
556.26/148.03 , isort^#(Cons(x, xs), r) -> insert^#(x, r)
556.26/148.03 , isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(1))
556.26/148.03
556.26/148.03 The following weak DPs constitute a sub-graph of the DG that is
556.26/148.03 closed under successors. The DPs are removed.
556.26/148.03
556.26/148.03 { insert^#(S(x), r) -> c_1(insert[Ite]^#(<(S(x), x), S(x), r))
556.26/148.03 , insert[Ite]^#(False(), x', Cons(x, xs)) -> c_4(insert^#(x', xs))
556.26/148.03 , isort^#(Cons(x, xs), r) -> insert^#(x, r)
556.26/148.03 , isort^#(Cons(x, xs), r) -> isort^#(xs, insert(x, r)) }
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(1)).
556.26/148.03
556.26/148.03 Weak Trs:
556.26/148.03 { insert[Ite](True(), x, r) -> Cons(x, r)
556.26/148.03 , insert[Ite](False(), x', Cons(x, xs)) -> Cons(x, insert(x', xs))
556.26/148.03 , insert(S(x), r) -> insert[Ite](<(S(x), x), S(x), r)
556.26/148.03 , <(x, 0()) -> False()
556.26/148.03 , <(S(x), S(y)) -> <(x, y)
556.26/148.03 , <(0(), S(y)) -> True() }
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(1))
556.26/148.03
556.26/148.03 No rule is usable, rules are removed from the input problem.
556.26/148.03
556.26/148.03 We are left with following problem, upon which TcT provides the
556.26/148.03 certificate YES(O(1),O(1)).
556.26/148.03
556.26/148.03 Rules: Empty
556.26/148.03 Obligation:
556.26/148.03 innermost runtime complexity
556.26/148.03 Answer:
556.26/148.03 YES(O(1),O(1))
556.26/148.03
556.26/148.03 Empty rules are trivially bounded
556.26/148.03
556.26/148.03 Hurray, we answered YES(O(1),O(n^2))
556.26/148.07 EOF