* Step 1: Sum WORST_CASE(Omega(n^1),O(n^2))
+ Considered Problem:
- Strict TRS:
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 TRS:
<(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:
{ 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 TRS:
<(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:
{ Cons(x,y)} =
isort(Cons(x,y),z) ->^+ isort(y,insert(x,z))
= C[isort(y,insert(x,z)) = isort(y,z){z -> insert(x,z)}]
** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
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 TRS:
<(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.
** Step 1.b:2: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
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()
- 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()
- Weak TRS:
<(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()
** Step 1.b:3: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
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()
- 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()
- Weak TRS:
<(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()
** Step 1.b:4: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
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))
- 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()
isort#(Nil(),r) -> c_5()
- Weak TRS:
<(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()
** Step 1.b:5: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
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))
- Weak DPs:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
- Weak TRS:
<(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)))
** Step 1.b:6: RemoveHeads WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
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))
- Weak DPs:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
- Weak TRS:
<(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())))]
** Step 1.b:7: Decompose WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
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))
- Weak DPs:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
- Weak TRS:
<(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()
- Weak DPs:
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:
<(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))
- Weak DPs:
insert#(x,Nil()) -> c_1()
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
- Weak TRS:
<(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()
- Weak DPs:
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:
<(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.
**** Step 1.b:7.a:1.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
insert#(x,Nil()) -> c_1()
- Weak DPs:
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:
<(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)) = [2]
>= [2]
= c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) = [2]
>= [2]
= c_9(insert#(x',xs))
isort#(Cons(x,xs),r) = [9] xs + [19]
>= [9] xs + [19]
= c_4(isort#(xs,insert(x,r)),insert#(x,r))
<(x,0()) = [1]
>= [1]
= False()
<(0(),S(y)) = [1]
>= [0]
= True()
<(S(x),S(y)) = [1]
>= [1]
= <(x,y)
**** Step 1.b:7.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
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:
<(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:
<(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()
**** Step 1.b:7.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
<(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))
- Weak DPs:
insert#(x,Nil()) -> c_1()
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
- Weak TRS:
<(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()
*** Step 1.b:7.b:2: Decompose WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
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))
- Weak DPs:
insert[Ite][False][Ite]#(False(),x',Cons(x,xs)) -> c_9(insert#(x',xs))
- Weak TRS:
<(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)))
- Weak DPs:
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:
<(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))
- Weak DPs:
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:
<(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)))
- Weak DPs:
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:
<(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}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.
***** Step 1.b:7.b:2.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
insert#(x',Cons(x,xs)) -> c_2(insert[Ite][False][Ite]#(<(x',x),x',Cons(x,xs)))
- Weak DPs:
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:
<(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 + 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(),x',Cons(x,xs)) = 2 + 2*xs
>= 1 + 2*xs
= c_9(insert#(x',xs))
isort#(Cons(x,xs),r) = 6 + 3*r + 3*r*xs + 6*xs + 2*xs^2
>= 4 + 2*r + 3*r*xs + 5*xs + 2*xs^2
= c_4(isort#(xs,insert(x,r)),insert#(x,r))
insert(x,Nil()) = 1
>= 1
= Cons(x,Nil())
insert(x',Cons(x,xs)) = 2 + xs
>= 2 + xs
= insert[Ite][False][Ite](<(x',x),x',Cons(x,xs))
insert[Ite][False][Ite](False(),x',Cons(x,xs)) = 2 + xs
>= 2 + xs
= Cons(x,insert(x',xs))
insert[Ite][False][Ite](True(),x,r) = 1 + r
>= 1 + r
= Cons(x,r)
***** Step 1.b:7.b:2.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
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:
<(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:
<(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))
***** Step 1.b:7.b:2.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
<(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))
- Weak DPs:
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:
<(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))
**** Step 1.b:7.b:2.b:2: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)),insert#(x,r))
- Weak TRS:
<(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)))
**** Step 1.b:7.b:2.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)))
- Weak TRS:
<(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.
***** Step 1.b:7.b:2.b:3.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)))
- Weak TRS:
<(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:
{ [4] xs + [14]
= c_4(isort#(xs,insert(x,r)))
Following rules are (at-least) weakly oriented:
***** Step 1.b:7.b:2.b:3.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
isort#(Cons(x,xs),r) -> c_4(isort#(xs,insert(x,r)))
- Weak TRS:
<(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:
<(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)))
***** Step 1.b:7.b:2.b:3.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
<(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:
{