*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
inssort(xs) -> isort(xs,Nil())
isort(Cons(x,xs),r) -> isort(xs,insert(x,r))
isort(Nil(),r) -> Nil()
Weak DP Rules:
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x))
inssort#(xs) -> c_2(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
isort#(Nil(),r) -> c_4()
Weak DPs
<#(x,0()) -> c_5()
<#(0(),S(y)) -> c_6()
<#(S(x),S(y)) -> c_7(<#(x,y))
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
insert[Ite]#(True(),x,r) -> c_9()
and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x))
inssort#(xs) -> c_2(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
isort#(Nil(),r) -> c_4()
Strict TRS Rules:
Weak DP Rules:
<#(x,0()) -> c_5()
<#(0(),S(y)) -> c_6()
<#(S(x),S(y)) -> c_7(<#(x,y))
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
insert[Ite]#(True(),x,r) -> c_9()
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[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) -> Nil()
Signature:
{ False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
<#(x,0()) -> c_5()
<#(0(),S(y)) -> c_6()
<#(S(x),S(y)) -> c_7(<#(x,y))
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x))
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
insert[Ite]#(True(),x,r) -> c_9()
inssort#(xs) -> c_2(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
isort#(Nil(),r) -> c_4()
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x))
inssort#(xs) -> c_2(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
isort#(Nil(),r) -> c_4()
Strict TRS Rules:
Weak DP Rules:
<#(x,0()) -> c_5()
<#(0(),S(y)) -> c_6()
<#(S(x),S(y)) -> c_7(<#(x,y))
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
insert[Ite]#(True(),x,r) -> c_9()
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{
c_1(insert[Ite]#(<(S(x),x)
,S(x)
,r)
,<#(S(x),x))
2: inssort#(xs) -> c_2(isort#(xs
,Nil()))
3: isort#(Cons(x,xs),r) ->
c_3(isort#(xs,insert(x,r))
,insert#(x,r))
4: isort#(Nil(),r) -> c_4()
5: <#(x,0()) -> c_5()
6: <#(0(),S(y)) -> c_6()
7: <#(S(x),S(y)) -> c_7(<#(x,y))
8: insert[Ite]#(False()
,x'
,Cons(x,xs)) -> c_8(insert#(x'
,xs))
9: insert[Ite]#(True(),x,r) ->
c_9()
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x))
inssort#(xs) -> c_2(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
<#(x,0()) -> c_5()
<#(0(),S(y)) -> c_6()
<#(S(x),S(y)) -> c_7(<#(x,y))
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
insert[Ite]#(True(),x,r) -> c_9()
isort#(Nil(),r) -> c_4()
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x))
-->_1 insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs)):7
-->_2 <#(S(x),S(y)) -> c_7(<#(x,y)):6
-->_1 insert[Ite]#(True(),x,r) -> c_9():8
-->_2 <#(x,0()) -> c_5():4
2:S:inssort#(xs) -> c_2(isort#(xs,Nil()))
-->_1 isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r)):3
-->_1 isort#(Nil(),r) -> c_4():9
3:S:isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Nil(),r) -> c_4():9
-->_1 isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r)):3
-->_2 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x)):1
4:W:<#(x,0()) -> c_5()
5:W:<#(0(),S(y)) -> c_6()
6:W:<#(S(x),S(y)) -> c_7(<#(x,y))
-->_1 <#(S(x),S(y)) -> c_7(<#(x,y)):6
-->_1 <#(0(),S(y)) -> c_6():5
-->_1 <#(x,0()) -> c_5():4
7:W:insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
-->_1 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x)):1
8:W:insert[Ite]#(True(),x,r) -> c_9()
9:W:isort#(Nil(),r) -> c_4()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: isort#(Nil(),r) -> c_4()
8: insert[Ite]#(True(),x,r) ->
c_9()
6: <#(S(x),S(y)) -> c_7(<#(x,y))
4: <#(x,0()) -> c_5()
5: <#(0(),S(y)) -> c_6()
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x))
inssort#(xs) -> c_2(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x))
-->_1 insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs)):7
2:S:inssort#(xs) -> c_2(isort#(xs,Nil()))
-->_1 isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r)):3
3:S:isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r)):3
-->_2 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x)):1
7:W:insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
-->_1 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r),<#(S(x),x)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r))
*** 1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r))
inssort#(xs) -> c_2(isort#(xs,Nil()))
isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1(insert[Ite]#(<(S(x),x),S(x),r))
-->_1 insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs)):4
2:S:inssort#(xs) -> c_2(isort#(xs,Nil()))
-->_1 isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r)):3
3:S:isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r)):3
-->_2 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r)):1
4:W:insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
-->_1 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r)):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).
[(2,inssort#(xs) -> c_2(isort#(xs,Nil())))]
*** 1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r))
isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1(insert[Ite]#(<(S(x),x),S(x),r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_3(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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_3(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r))
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1(insert[Ite]#(<(S(x),x),S(x),r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_3(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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{
c_1(insert[Ite]#(<(S(x),x)
,S(x)
,r))
Consider the set of all dependency pairs
1: insert#(S(x),r) ->
c_1(insert[Ite]#(<(S(x),x)
,S(x)
,r))
3: isort#(Cons(x,xs),r) ->
c_3(isort#(xs,insert(x,r))
,insert#(x,r))
4: insert[Ite]#(False()
,x'
,Cons(x,xs)) -> c_8(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.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r))
Strict TRS Rules:
Weak DP Rules:
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_3(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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ 2*r
= c_1(insert[Ite]#(<(S(x),x)
,S(x)
,r))
Following rules are (at-least) weakly oriented:
insert[Ite]#(False() = 2 + 2*x' + 2*x'*xs + 2*xs
,x'
,Cons(x,xs))
>= 1 + 2*xs
= c_8(insert#(x',xs))
isort#(Cons(x,xs),r) = 6 + 2*r + 2*r*xs + 6*xs + 2*xs^2
>= 3 + 2*r + 2*r*xs + 6*xs + 2*xs^2
= c_3(isort#(xs,insert(x,r))
,insert#(x,r))
insert(S(x),r) = 2 + r
>= 2 + r
= insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False() = 3 + xs
,x'
,Cons(x,xs))
>= 3 + xs
= Cons(x,insert(x',xs))
insert[Ite](True(),x,r) = 2 + r
>= 1 + r
= Cons(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#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r))
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_3(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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1(insert[Ite]#(<(S(x),x),S(x),r))
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
isort#(Cons(x,xs),r) -> c_3(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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_1(insert[Ite]#(<(S(x),x),S(x),r))
-->_1 insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs)):2
2:W:insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
-->_1 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r)):1
3:W:isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r)):3
-->_2 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r)):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_3(isort#(xs,insert(x,r))
,insert#(x,r))
1: insert#(S(x),r) ->
c_1(insert[Ite]#(<(S(x),x)
,S(x)
,r))
2: insert[Ite]#(False()
,x'
,Cons(x,xs)) -> c_8(insert#(x'
,xs))
*** 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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_3(isort#(xs,insert(x,r)),insert#(x,r))
Strict TRS Rules:
Weak DP Rules:
insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r))
insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_3(isort#(xs,insert(x,r)),insert#(x,r))
-->_2 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r)):2
-->_1 isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)),insert#(x,r)):1
2:W:insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r))
-->_1 insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs)):3
3:W:insert[Ite]#(False(),x',Cons(x,xs)) -> c_8(insert#(x',xs))
-->_1 insert#(S(x),r) -> c_1(insert[Ite]#(<(S(x),x),S(x),r)):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
2: insert#(S(x),r) ->
c_1(insert[Ite]#(<(S(x),x)
,S(x)
,r))
3: insert[Ite]#(False()
,x'
,Cons(x,xs)) -> c_8(insert#(x'
,xs))
*** 1.1.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isort#(Cons(x,xs),r) -> c_3(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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_3(isort#(xs,insert(x,r)),insert#(x,r))
-->_1 isort#(Cons(x,xs),r) -> c_3(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_3(isort#(xs,insert(x,r)))
*** 1.1.1.1.1.1.1.2.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isort#(Cons(x,xs),r) -> c_3(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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{
c_3(isort#(xs,insert(x,r)))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.1.1.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
isort#(Cons(x,xs),r) -> c_3(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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ [8] xs + [12]
= c_3(isort#(xs,insert(x,r)))
Following rules are (at-least) weakly oriented:
*** 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:
isort#(Cons(x,xs),r) -> c_3(isort#(xs,insert(x,r)))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_3(isort#(xs,insert(x,r)))
Weak TRS Rules:
<(x,0()) -> False()
<(0(),S(y)) -> True()
<(S(x),S(y)) -> <(x,y)
insert(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{ c_3(isort#(xs,insert(x,r)))
-->_1 isort#(Cons(x,xs),r) -> c_3(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_3(isort#(xs,insert(x,r)))
*** 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(S(x),r) -> insert[Ite](<(S(x),x),S(x),r)
insert[Ite](False(),x',Cons(x,xs)) -> Cons(x,insert(x',xs))
insert[Ite](True(),x,r) -> Cons(x,r)
Signature:
{