*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
inssort(xs) -> isort(xs,Nil())
isort(Cons(x,xs),r) -> isort(xs,insert(x,r))
isort(Nil(),r) -> r
Weak DP Rules:
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
inssort#(xs) -> c_3(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
isort#(Nil(),r) -> c_5()
Weak DPs
<#(x,0()) -> c_6()
<#(0(),S(y)) -> c_7()
<#(S(x),S(y)) -> c_8(<#(x,y))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
insert[Ite][False][Ite]#(True(),x,r) -> c_10()
and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(x,Nil()) -> c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
inssort#(xs) -> c_3(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
isort#(Nil(),r) -> c_5()
Strict TRS Rules:
Weak DP Rules:
<#(x,0()) -> c_6()
<#(0(),S(y)) -> c_7()
<#(S(x),S(y)) -> c_8(<#(x,y))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
insert[Ite][False][Ite]#(True(),x,r) -> c_10()
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
inssort(xs) -> isort(xs,Nil())
isort(Cons(x,xs),r) -> isort(xs,insert(x,r))
isort(Nil(),r) -> r
Signature:
{ False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
<#(x,0()) -> c_6()
<#(0(),S(y)) -> c_7()
<#(S(x),S(y)) -> c_8(<#(x,y))
insert#(x,Nil()) -> c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
insert[Ite][False][Ite]#(True(),x,r) -> c_10()
inssort#(xs) -> c_3(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
isort#(Nil(),r) -> c_5()
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(x,Nil()) -> c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
inssort#(xs) -> c_3(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
isort#(Nil(),r) -> c_5()
Strict TRS Rules:
Weak DP Rules:
<#(x,0()) -> c_6()
<#(0(),S(y)) -> c_7()
<#(S(x),S(y)) -> c_8(<#(x,y))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
insert[Ite][False][Ite]#(True(),x,r) -> c_10()
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
2: insert#(x',Cons(x,xs)) ->
c_2(insert[Ite][False][Ite]#(<(x'
,x)
,x'
,Cons(x,xs))
,<#(x',x))
3: inssort#(xs) -> c_3(isort#(xs
,Nil()))
4: isort#(Cons(x,xs),r) ->
c_4(isort#(xs,insert(x,r))
,insert#(x,r))
5: isort#(Nil(),r) -> c_5()
6: <#(x,0()) -> c_6()
7: <#(0(),S(y)) -> c_7()
8: <#(S(x),S(y)) -> c_8(<#(x,y))
9: insert[Ite][False][Ite]#(False()
,x'
,Cons(x,xs)) -> c_9(insert#(x'
,xs))
10: insert[Ite][False][Ite]#(True()
,x
,r) -> c_10()
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(x,Nil()) -> c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
inssort#(xs) -> c_3(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
<#(x,0()) -> c_6()
<#(0(),S(y)) -> c_7()
<#(S(x),S(y)) -> c_8(<#(x,y))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
insert[Ite][False][Ite]#(True(),x,r) -> c_10()
isort#(Nil(),r) -> c_5()
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
2:S:insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
-->_1 insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs)):8
-->_2 <#(S(x),S(y)) -> c_8(<#(x,y)):7
-->_1 insert[Ite][False][Ite]#(True(),x,r) -> c_10():9
-->_2 <#(0(),S(y)) -> c_7():6
-->_2 <#(x,0()) -> c_6():5
3:S:inssort#(xs) -> c_3(isort#(xs,Nil()))
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):4
-->_1 isort#(Nil(),r) -> c_5():10
4:S:isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Nil(),r) -> c_5():10
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):4
-->_2 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):2
-->_2 insert#(x,Nil()) -> c_1():1
5:W:<#(x,0()) -> c_6()
6:W:<#(0(),S(y)) -> c_7()
7:W:<#(S(x),S(y)) -> c_8(<#(x,y))
-->_1 <#(S(x),S(y)) -> c_8(<#(x,y)):7
-->_1 <#(0(),S(y)) -> c_7():6
-->_1 <#(x,0()) -> c_6():5
8:W:insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
-->_1 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):2
-->_1 insert#(x,Nil()) -> c_1():1
9:W:insert[Ite][False][Ite]#(True(),x,r) -> c_10()
10:W:isort#(Nil(),r) -> c_5()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
10: isort#(Nil(),r) -> c_5()
9: insert[Ite][False][Ite]#(True()
,x
,r) -> c_10()
7: <#(S(x),S(y)) -> c_8(<#(x,y))
5: <#(x,0()) -> c_6()
6: <#(0(),S(y)) -> c_7()
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(x,Nil()) -> c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
inssort#(xs) -> c_3(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
2:S:insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x))
-->_1 insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs)):8
3:S:inssort#(xs) -> c_3(isort#(xs,Nil()))
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):4
4:S:isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):4
-->_2 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):2
-->_2 insert#(x,Nil()) -> c_1():1
8:W:insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
-->_1 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)),<#(x',x)):2
-->_1 insert#(x,Nil()) -> c_1():1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
*** 1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(x,Nil()) -> c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
inssort#(xs) -> c_3(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
2:S:insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs)):5
3:S:inssort#(xs) -> c_3(isort#(xs,Nil()))
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):4
4:S:isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):4
-->_2 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):2
-->_2 insert#(x,Nil()) -> c_1():1
5:W:insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
-->_1 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):2
-->_1 insert#(x,Nil()) -> c_1():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).
[(3,inssort#(xs) -> c_3(isort#(xs,Nil())))]
*** 1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(x,Nil()) -> c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
Strict TRS Rules:
Weak DP Rules:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert#(x,Nil()) -> c_1()
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
Strict TRS Rules:
Weak DP Rules:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
insert#(x,Nil()) -> c_1()
Strict TRS Rules:
Weak DP Rules:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ [0]
= c_1()
Following rules are (at-least) weakly oriented:
insert#(x',Cons(x,xs)) = [1]
>= [1]
= c_2(insert[Ite][False][Ite]#(<(x'
,x)
,x'
,Cons(x,xs)))
insert[Ite][False][Ite]#(False() = [1]
,x'
,Cons(x,xs))
>= [1]
= c_9(insert#(x',xs))
isort#(Cons(x,xs),r) = [1] x + [1] xs + [1]
>= [1] xs + [1]
= c_4(isort#(xs,insert(x,r))
,insert#(x,r))
*** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
insert#(x,Nil()) -> c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1()
2:W:insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs)):3
3:W:insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
-->_1 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):2
-->_1 insert#(x,Nil()) -> c_1():1
4:W:isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):4
-->_2 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):2
-->_2 insert#(x,Nil()) -> c_1():1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
4: isort#(Cons(x,xs),r) ->
c_4(isort#(xs,insert(x,r))
,insert#(x,r))
2: insert#(x',Cons(x,xs)) ->
c_2(insert[Ite][False][Ite]#(<(x'
,x)
,x'
,Cons(x,xs)))
3: insert[Ite][False][Ite]#(False()
,x'
,Cons(x,xs)) -> c_9(insert#(x'
,xs))
1: insert#(x,Nil()) -> c_1()
*** 1.1.1.1.1.1.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert#(x,Nil()) -> c_1()
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs)):4
2:S:isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
-->_2 insert#(x,Nil()) -> c_1():3
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):2
-->_2 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):1
3:W:insert#(x,Nil()) -> c_1()
4:W:insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
-->_1 insert#(x,Nil()) -> c_1():3
-->_1 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: insert#(x,Nil()) -> c_1()
*** 1.1.1.1.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Strict TRS Rules:
Weak DP Rules:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Strict TRS Rules:
Weak DP Rules:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{
c_2(insert[Ite][False][Ite]#(<(x'
,x)
,x'
,Cons(x,xs)))
Consider the set of all dependency pairs
1: insert#(x',Cons(x,xs)) ->
c_2(insert[Ite][False][Ite]#(<(x'
,x)
,x'
,Cons(x,xs)))
2: isort#(Cons(x,xs),r) ->
c_4(isort#(xs,insert(x,r))
,insert#(x,r))
4: insert[Ite][False][Ite]#(False()
,x'
,Cons(x,xs)) -> c_9(insert#(x'
,xs))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,4}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
Strict TRS Rules:
Weak DP Rules:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ 2 + xs
= c_2(insert[Ite][False][Ite]#(<(x'
,x)
,x'
,Cons(x,xs)))
Following rules are (at-least) weakly oriented:
insert[Ite][False][Ite]#(False() = 2 + xs
,x'
,Cons(x,xs))
>= 2 + xs
= c_9(insert#(x',xs))
isort#(Cons(x,xs),r) = 6 + 2*r + 2*r*xs + 6*xs + 2*xs^2
>= 5 + r + 2*r*xs + 6*xs + 2*xs^2
= c_4(isort#(xs,insert(x,r))
,insert#(x,r))
insert(x,Nil()) = 2
>= 1
= Cons(x,Nil())
insert(x',Cons(x,xs)) = 3 + xs
>= 3 + xs
= insert[Ite][False][Ite](<(x',x)
,x'
,Cons(x,xs))
insert[Ite][False][Ite](False() = 3 + xs
,x'
,Cons(x,xs))
>= 3 + xs
= Cons(x,insert(x',xs))
insert[Ite][False][Ite](True() = 2 + r
,x
,r)
>= 1 + r
= Cons(x,r)
*** 1.1.1.1.1.1.1.2.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs)):2
2:W:insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
-->_1 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):1
3:W:isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):3
-->_2 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: isort#(Cons(x,xs),r) ->
c_4(isort#(xs,insert(x,r))
,insert#(x,r))
1: insert#(x',Cons(x,xs)) ->
c_2(insert[Ite][False][Ite]#(<(x'
,x)
,x'
,Cons(x,xs)))
2: insert[Ite][False][Ite]#(False()
,x'
,Cons(x,xs)) -> c_9(insert#(x'
,xs))
*** 1.1.1.1.1.1.1.2.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_4(isort#(xs,insert(x,r)),insert#(x,r))
-->_2 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):2
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):1
2:W:insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
-->_1 insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs)):3
3:W:insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
-->_1 insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs))):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
2: insert#(x',Cons(x,xs)) ->
c_2(insert[Ite][False][Ite]#(<(x'
,x)
,x'
,Cons(x,xs)))
3: insert[Ite][False][Ite]#(False()
,x'
,Cons(x,xs)) -> c_9(insert#(x'
,xs))
*** 1.1.1.1.1.1.1.2.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_4(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)))
*** 1.1.1.1.1.1.1.2.1.2.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{
c_4(isort#(xs,insert(x,r)))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.1.1.2.1.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ [1] r + [8] xs + [16]
= c_4(isort#(xs,insert(x,r)))
Following rules are (at-least) weakly oriented:
insert(x,Nil()) = [7]
>= [3]
= Cons(x,Nil())
insert(x',Cons(x,xs)) = [1] xs + [10]
>= [1] xs + [10]
= insert[Ite][False][Ite](<(x',x)
,x'
,Cons(x,xs))
insert[Ite][False][Ite](False() = [1] xs + [10]
,x'
,Cons(x,xs))
>= [1] xs + [10]
= Cons(x,insert(x',xs))
insert[Ite][False][Ite](True() = [1] r + [7]
,x
,r)
>= [1] r + [3]
= Cons(x,r)
*** 1.1.1.1.1.1.1.2.1.2.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_4(isort#(xs,insert(x,r)))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_4(isort#(xs,insert(x,r)))
-->_1 isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r))):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: isort#(Cons(x,xs),r) ->
c_4(isort#(xs,insert(x,r)))
*** 1.1.1.1.1.1.1.2.1.2.1.1.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(x,Nil()) -> Cons(x,Nil())
insert(x',Cons(x,xs)) -> insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) -> Cons(x,r)
Signature:
{