*** 1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
sort(cons(n,x)) -> cons(min(cons(n,x)),sort(replace(min(cons(n,x)),n,x)))
sort(nil()) -> nil()
Weak DP Rules:
Weak TRS Rules:
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0}
Obligation:
Innermost
basic terms: {eq,if_min,if_replace,le,min,replace,sort}/{0,cons,false,nil,s,true}
Applied Processor:
DependencyPairs {dpKind_ = DT}
Proof:
We add the following dependency tuples:
Strict DPs
eq#(0(),0()) -> c_1()
eq#(0(),s(m)) -> c_2()
eq#(s(n),0()) -> c_3()
eq#(s(n),s(m)) -> c_4(eq#(n,m))
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
if_replace#(true(),n,m,cons(k,x)) -> c_8()
le#(0(),m) -> c_9()
le#(s(n),0()) -> c_10()
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
min#(cons(0(),nil())) -> c_13()
min#(cons(s(n),nil())) -> c_14()
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
replace#(n,m,nil()) -> c_16()
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
sort#(nil()) -> c_18()
Weak DPs
and mark the set of starting terms.
*** 1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
eq#(0(),0()) -> c_1()
eq#(0(),s(m)) -> c_2()
eq#(s(n),0()) -> c_3()
eq#(s(n),s(m)) -> c_4(eq#(n,m))
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
if_replace#(true(),n,m,cons(k,x)) -> c_8()
le#(0(),m) -> c_9()
le#(s(n),0()) -> c_10()
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
min#(cons(0(),nil())) -> c_13()
min#(cons(s(n),nil())) -> c_14()
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
replace#(n,m,nil()) -> c_16()
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
sort#(nil()) -> c_18()
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
sort(cons(n,x)) -> cons(min(cons(n,x)),sort(replace(min(cons(n,x)),n,x)))
sort(nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
UsableRules
Proof:
We replace rewrite rules by usable rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
eq#(0(),0()) -> c_1()
eq#(0(),s(m)) -> c_2()
eq#(s(n),0()) -> c_3()
eq#(s(n),s(m)) -> c_4(eq#(n,m))
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
if_replace#(true(),n,m,cons(k,x)) -> c_8()
le#(0(),m) -> c_9()
le#(s(n),0()) -> c_10()
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
min#(cons(0(),nil())) -> c_13()
min#(cons(s(n),nil())) -> c_14()
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
replace#(n,m,nil()) -> c_16()
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
sort#(nil()) -> c_18()
*** 1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
eq#(0(),0()) -> c_1()
eq#(0(),s(m)) -> c_2()
eq#(s(n),0()) -> c_3()
eq#(s(n),s(m)) -> c_4(eq#(n,m))
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
if_replace#(true(),n,m,cons(k,x)) -> c_8()
le#(0(),m) -> c_9()
le#(s(n),0()) -> c_10()
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
min#(cons(0(),nil())) -> c_13()
min#(cons(s(n),nil())) -> c_14()
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
replace#(n,m,nil()) -> c_16()
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
sort#(nil()) -> c_18()
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
Proof:
We estimate the number of application of
{1,2,3,8,9,10,13,14,16,18}
by application of
Pre({1,2,3,8,9,10,13,14,16,18}) = {4,5,6,7,11,12,15,17}.
Here rules are labelled as follows:
1: eq#(0(),0()) -> c_1()
2: eq#(0(),s(m)) -> c_2()
3: eq#(s(n),0()) -> c_3()
4: eq#(s(n),s(m)) -> c_4(eq#(n,m))
5: if_min#(false()
,cons(n,cons(m,x))) ->
c_5(min#(cons(m,x)))
6: if_min#(true()
,cons(n,cons(m,x))) ->
c_6(min#(cons(n,x)))
7: if_replace#(false()
,n
,m
,cons(k,x)) -> c_7(replace#(n
,m
,x))
8: if_replace#(true()
,n
,m
,cons(k,x)) -> c_8()
9: le#(0(),m) -> c_9()
10: le#(s(n),0()) -> c_10()
11: le#(s(n),s(m)) -> c_11(le#(n,m))
12: min#(cons(n,cons(m,x))) ->
c_12(if_min#(le(n,m)
,cons(n,cons(m,x)))
,le#(n,m))
13: min#(cons(0(),nil())) -> c_13()
14: min#(cons(s(n),nil())) -> c_14()
15: replace#(n,m,cons(k,x)) ->
c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x))
,eq#(n,k))
16: replace#(n,m,nil()) -> c_16()
17: sort#(cons(n,x)) ->
c_17(min#(cons(n,x))
,sort#(replace(min(cons(n,x))
,n
,x))
,replace#(min(cons(n,x)),n,x)
,min#(cons(n,x)))
18: sort#(nil()) -> c_18()
*** 1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
eq#(0(),0()) -> c_1()
eq#(0(),s(m)) -> c_2()
eq#(s(n),0()) -> c_3()
if_replace#(true(),n,m,cons(k,x)) -> c_8()
le#(0(),m) -> c_9()
le#(s(n),0()) -> c_10()
min#(cons(0(),nil())) -> c_13()
min#(cons(s(n),nil())) -> c_14()
replace#(n,m,nil()) -> c_16()
sort#(nil()) -> c_18()
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:eq#(s(n),s(m)) -> c_4(eq#(n,m))
-->_1 eq#(s(n),0()) -> c_3():11
-->_1 eq#(0(),s(m)) -> c_2():10
-->_1 eq#(0(),0()) -> c_1():9
-->_1 eq#(s(n),s(m)) -> c_4(eq#(n,m)):1
2:S:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):6
-->_1 min#(cons(s(n),nil())) -> c_14():16
-->_1 min#(cons(0(),nil())) -> c_13():15
3:S:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):6
-->_1 min#(cons(s(n),nil())) -> c_14():16
-->_1 min#(cons(0(),nil())) -> c_13():15
4:S:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):7
-->_1 replace#(n,m,nil()) -> c_16():17
5:S:le#(s(n),s(m)) -> c_11(le#(n,m))
-->_1 le#(s(n),0()) -> c_10():14
-->_1 le#(0(),m) -> c_9():13
-->_1 le#(s(n),s(m)) -> c_11(le#(n,m)):5
6:S:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
-->_2 le#(s(n),0()) -> c_10():14
-->_2 le#(0(),m) -> c_9():13
-->_2 le#(s(n),s(m)) -> c_11(le#(n,m)):5
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):3
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):2
7:S:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
-->_1 if_replace#(true(),n,m,cons(k,x)) -> c_8():12
-->_2 eq#(s(n),0()) -> c_3():11
-->_2 eq#(0(),s(m)) -> c_2():10
-->_2 eq#(0(),0()) -> c_1():9
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):4
-->_2 eq#(s(n),s(m)) -> c_4(eq#(n,m)):1
8:S:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
-->_2 sort#(nil()) -> c_18():18
-->_3 replace#(n,m,nil()) -> c_16():17
-->_4 min#(cons(s(n),nil())) -> c_14():16
-->_1 min#(cons(s(n),nil())) -> c_14():16
-->_4 min#(cons(0(),nil())) -> c_13():15
-->_1 min#(cons(0(),nil())) -> c_13():15
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x))):8
-->_3 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):7
-->_4 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):6
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):6
9:W:eq#(0(),0()) -> c_1()
10:W:eq#(0(),s(m)) -> c_2()
11:W:eq#(s(n),0()) -> c_3()
12:W:if_replace#(true(),n,m,cons(k,x)) -> c_8()
13:W:le#(0(),m) -> c_9()
14:W:le#(s(n),0()) -> c_10()
15:W:min#(cons(0(),nil())) -> c_13()
16:W:min#(cons(s(n),nil())) -> c_14()
17:W:replace#(n,m,nil()) -> c_16()
18:W:sort#(nil()) -> c_18()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
18: sort#(nil()) -> c_18()
17: replace#(n,m,nil()) -> c_16()
12: if_replace#(true()
,n
,m
,cons(k,x)) -> c_8()
15: min#(cons(0(),nil())) -> c_13()
16: min#(cons(s(n),nil())) -> c_14()
13: le#(0(),m) -> c_9()
14: le#(s(n),0()) -> c_10()
9: eq#(0(),0()) -> c_1()
10: eq#(0(),s(m)) -> c_2()
11: eq#(s(n),0()) -> c_3()
*** 1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
Proof:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
Strict DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
Strict TRS Rules:
Weak DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Problem (S)
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
*** 1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
Strict TRS Rules:
Weak DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:eq#(s(n),s(m)) -> c_4(eq#(n,m))
-->_1 eq#(s(n),s(m)) -> c_4(eq#(n,m)):1
2:W:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):6
3:W:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):6
4:W:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):7
5:W:le#(s(n),s(m)) -> c_11(le#(n,m))
-->_1 le#(s(n),s(m)) -> c_11(le#(n,m)):5
6:W:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
-->_2 le#(s(n),s(m)) -> c_11(le#(n,m)):5
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):3
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):2
7:W:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):4
-->_2 eq#(s(n),s(m)) -> c_4(eq#(n,m)):1
8:W:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
-->_4 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):6
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):6
-->_3 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):7
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x))):8
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
2: if_min#(false()
,cons(n,cons(m,x))) ->
c_5(min#(cons(m,x)))
6: min#(cons(n,cons(m,x))) ->
c_12(if_min#(le(n,m)
,cons(n,cons(m,x)))
,le#(n,m))
3: if_min#(true()
,cons(n,cons(m,x))) ->
c_6(min#(cons(n,x)))
5: le#(s(n),s(m)) -> c_11(le#(n,m))
*** 1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:eq#(s(n),s(m)) -> c_4(eq#(n,m))
-->_1 eq#(s(n),s(m)) -> c_4(eq#(n,m)):1
4:W:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):7
7:W:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):4
-->_2 eq#(s(n),s(m)) -> c_4(eq#(n,m)):1
8:W:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
-->_3 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):7
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x))):8
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
*** 1.1.1.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing}
Proof:
We decompose the input problem according to the dependency graph into the upper component
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
and a lower component
eq#(s(n),s(m)) -> c_4(eq#(n,m))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
Further, following extension rules are added to the lower component.
sort#(cons(n,x)) -> replace#(min(cons(n,x)),n,x)
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
*** 1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: sort#(cons(n,x)) ->
c_17(sort#(replace(min(cons(n
,x))
,n
,x))
,replace#(min(cons(n,x)),n,x))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_17) = {1,2}
Following symbols are considered usable:
{if_replace,replace,eq#,if_min#,if_replace#,le#,min#,replace#,sort#}
TcT has computed the following interpretation:
p(0) = [4]
p(cons) = [1] x2 + [2]
p(eq) = [0]
p(false) = [0]
p(if_min) = [0]
p(if_replace) = [1] x4 + [0]
p(le) = [1] x1 + [0]
p(min) = [1]
p(nil) = [2]
p(replace) = [1] x3 + [0]
p(s) = [1]
p(sort) = [2]
p(true) = [0]
p(eq#) = [1] x1 + [1]
p(if_min#) = [1] x2 + [2]
p(if_replace#) = [1] x1 + [2] x3 + [1] x4 + [1]
p(le#) = [2] x1 + [1]
p(min#) = [1] x1 + [4]
p(replace#) = [1]
p(sort#) = [2] x1 + [2]
p(c_1) = [1]
p(c_2) = [2]
p(c_3) = [1]
p(c_4) = [1]
p(c_5) = [2]
p(c_6) = [1]
p(c_7) = [1]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
p(c_11) = [0]
p(c_12) = [1] x1 + [1] x2 + [0]
p(c_13) = [4]
p(c_14) = [0]
p(c_15) = [1] x1 + [0]
p(c_16) = [4]
p(c_17) = [1] x1 + [2] x2 + [1]
p(c_18) = [1]
Following rules are strictly oriented:
sort#(cons(n,x)) = [2] x + [6]
> [2] x + [5]
= c_17(sort#(replace(min(cons(n
,x))
,n
,x))
,replace#(min(cons(n,x)),n,x))
Following rules are (at-least) weakly oriented:
if_replace(false() = [1] x + [2]
,n
,m
,cons(k,x))
>= [1] x + [2]
= cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) = [1] x + [2]
>= [1] x + [2]
= cons(m,x)
replace(n,m,cons(k,x)) = [1] x + [2]
>= [1] x + [2]
= if_replace(eq(n,k)
,n
,m
,cons(k,x))
replace(n,m,nil()) = [2]
>= [2]
= nil()
*** 1.1.1.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
-->_1 sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: sort#(cons(n,x)) ->
c_17(sort#(replace(min(cons(n
,x))
,n
,x))
,replace#(min(cons(n,x)),n,x))
*** 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:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.1.1.1.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> replace#(min(cons(n,x)),n,x)
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: eq#(s(n),s(m)) -> c_4(eq#(n,m))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> replace#(min(cons(n,x)),n,x)
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_4) = {1},
uargs(c_7) = {1},
uargs(c_15) = {1,2}
Following symbols are considered usable:
{if_replace,replace,eq#,if_min#,if_replace#,le#,min#,replace#,sort#}
TcT has computed the following interpretation:
p(0) = [0]
[2]
p(cons) = [0 0] x1 + [0 1] x2 + [0]
[0 1] [0 1] [0]
p(eq) = [2 0] x1 + [0 0] x2 + [0]
[0 0] [2 0] [2]
p(false) = [0]
[0]
p(if_min) = [1 2] x1 + [0]
[0 0] [1]
p(if_replace) = [1 1] x3 + [0 1] x4 + [0]
[0 1] [0 1] [0]
p(le) = [2 0] x1 + [1 0] x2 + [0]
[0 0] [1 0] [0]
p(min) = [0]
[2]
p(nil) = [0]
[0]
p(replace) = [2 2] x2 + [0 2] x3 + [0]
[0 1] [0 1] [0]
p(s) = [0 2] x1 + [2]
[0 1] [1]
p(sort) = [0]
[2]
p(true) = [1]
[0]
p(eq#) = [0 1] x2 + [0]
[0 1] [0]
p(if_min#) = [1 1] x2 + [2]
[0 2] [0]
p(if_replace#) = [0 0] x2 + [2 0] x4 + [0]
[1 0] [1 0] [1]
p(le#) = [1 2] x1 + [0 1] x2 + [1]
[0 0] [0 0] [0]
p(min#) = [0]
[2]
p(replace#) = [0 2] x3 + [0]
[0 2] [2]
p(sort#) = [0 2] x1 + [0]
[0 2] [2]
p(c_1) = [0]
[1]
p(c_2) = [0]
[0]
p(c_3) = [0]
[0]
p(c_4) = [1 0] x1 + [0]
[0 0] [1]
p(c_5) = [0]
[0]
p(c_6) = [0 0] x1 + [2]
[2 2] [0]
p(c_7) = [1 0] x1 + [0]
[0 0] [1]
p(c_8) = [2]
[2]
p(c_9) = [0]
[1]
p(c_10) = [1]
[0]
p(c_11) = [0 0] x1 + [1]
[0 1] [0]
p(c_12) = [0 2] x2 + [0]
[0 0] [1]
p(c_13) = [0]
[1]
p(c_14) = [0]
[2]
p(c_15) = [1 0] x1 + [1 1] x2 + [0]
[1 0] [0 2] [0]
p(c_16) = [2]
[2]
p(c_17) = [0 0] x2 + [0]
[0 2] [2]
p(c_18) = [1]
[0]
Following rules are strictly oriented:
eq#(s(n),s(m)) = [0 1] m + [1]
[0 1] [1]
> [0 1] m + [0]
[0 0] [1]
= c_4(eq#(n,m))
Following rules are (at-least) weakly oriented:
if_replace#(false() = [0 0] n + [0 2] x + [0]
,n [1 0] [0 1] [1]
,m
,cons(k,x))
>= [0 2] x + [0]
[0 0] [1]
= c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) = [0 2] k + [0 2] x + [0]
[0 2] [0 2] [2]
>= [0 2] k + [0 2] x + [0]
[0 2] [0 2] [0]
= c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x))
,eq#(n,k))
sort#(cons(n,x)) = [0 2] n + [0 2] x + [0]
[0 2] [0 2] [2]
>= [0 2] x + [0]
[0 2] [2]
= replace#(min(cons(n,x)),n,x)
sort#(cons(n,x)) = [0 2] n + [0 2] x + [0]
[0 2] [0 2] [2]
>= [0 2] n + [0 2] x + [0]
[0 2] [0 2] [2]
= sort#(replace(min(cons(n,x))
,n
,x))
if_replace(false() = [0 1] k + [1 1] m + [0
,n 1] x + [0]
,m [0 1] [0 1] [0
,cons(k,x)) 1] [0]
>= [0 0] k + [0 1] m + [0
1] x + [0]
[0 1] [0 1] [0
1] [0]
= cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) = [0 1] k + [1 1] m + [0
1] x + [0]
[0 1] [0 1] [0
1] [0]
>= [0 0] m + [0 1] x + [0]
[0 1] [0 1] [0]
= cons(m,x)
replace(n,m,cons(k,x)) = [0 2] k + [2 2] m + [0
2] x + [0]
[0 1] [0 1] [0
1] [0]
>= [0 1] k + [1 1] m + [0
1] x + [0]
[0 1] [0 1] [0
1] [0]
= if_replace(eq(n,k)
,n
,m
,cons(k,x))
replace(n,m,nil()) = [2 2] m + [0]
[0 1] [0]
>= [0]
[0]
= nil()
*** 1.1.1.1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> replace#(min(cons(n,x)),n,x)
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.1.1.1.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> replace#(min(cons(n,x)),n,x)
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:eq#(s(n),s(m)) -> c_4(eq#(n,m))
-->_1 eq#(s(n),s(m)) -> c_4(eq#(n,m)):1
2:W:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):3
3:W:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):2
-->_2 eq#(s(n),s(m)) -> c_4(eq#(n,m)):1
4:W:sort#(cons(n,x)) -> replace#(min(cons(n,x)),n,x)
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):3
5:W:sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
-->_1 sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x)):5
-->_1 sort#(cons(n,x)) -> replace#(min(cons(n,x)),n,x):4
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
5: sort#(cons(n,x)) ->
sort#(replace(min(cons(n,x))
,n
,x))
4: sort#(cons(n,x)) ->
replace#(min(cons(n,x)),n,x)
2: if_replace#(false()
,n
,m
,cons(k,x)) -> c_7(replace#(n
,m
,x))
3: replace#(n,m,cons(k,x)) ->
c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x))
,eq#(n,k))
1: eq#(s(n),s(m)) -> c_4(eq#(n,m))
*** 1.1.1.1.1.1.1.1.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
eq#(s(n),s(m)) -> c_4(eq#(n,m))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
2:S:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
3:S:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):6
4:S:le#(s(n),s(m)) -> c_11(le#(n,m))
-->_1 le#(s(n),s(m)) -> c_11(le#(n,m)):4
5:S:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
-->_2 le#(s(n),s(m)) -> c_11(le#(n,m)):4
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):2
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):1
6:S:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
-->_2 eq#(s(n),s(m)) -> c_4(eq#(n,m)):8
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):3
7:S:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x))):7
-->_3 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):6
-->_4 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
8:W:eq#(s(n),s(m)) -> c_4(eq#(n,m))
-->_1 eq#(s(n),s(m)) -> c_4(eq#(n,m)):8
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
8: eq#(s(n),s(m)) -> c_4(eq#(n,m))
*** 1.1.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/2,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
2:S:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
3:S:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):6
4:S:le#(s(n),s(m)) -> c_11(le#(n,m))
-->_1 le#(s(n),s(m)) -> c_11(le#(n,m)):4
5:S:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
-->_2 le#(s(n),s(m)) -> c_11(le#(n,m)):4
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):2
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):1
6:S:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k))
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):3
7:S:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x))):7
-->_3 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)),eq#(n,k)):6
-->_4 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
*** 1.1.1.1.1.2.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
Proof:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Problem (S)
Strict DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
*** 1.1.1.1.1.2.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
2:S:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
3:W:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):6
4:S:le#(s(n),s(m)) -> c_11(le#(n,m))
-->_1 le#(s(n),s(m)) -> c_11(le#(n,m)):4
5:S:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
-->_2 le#(s(n),s(m)) -> c_11(le#(n,m)):4
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):2
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):1
6:W:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):3
7:W:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
-->_4 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
-->_3 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):6
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x))):7
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: if_replace#(false()
,n
,m
,cons(k,x)) -> c_7(replace#(n
,m
,x))
6: replace#(n,m,cons(k,x)) ->
c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x)))
*** 1.1.1.1.1.2.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
2:S:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
4:S:le#(s(n),s(m)) -> c_11(le#(n,m))
-->_1 le#(s(n),s(m)) -> c_11(le#(n,m)):4
5:S:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
-->_2 le#(s(n),s(m)) -> c_11(le#(n,m)):4
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):2
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):1
7:W:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
-->_4 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):5
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x))):7
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),min#(cons(n,x)))
*** 1.1.1.1.1.2.1.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),min#(cons(n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing}
Proof:
We decompose the input problem according to the dependency graph into the upper component
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),min#(cons(n,x)))
and a lower component
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Further, following extension rules are added to the lower component.
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
*** 1.1.1.1.1.2.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: sort#(cons(n,x)) ->
c_17(min#(cons(n,x))
,sort#(replace(min(cons(n,x))
,n
,x))
,min#(cons(n,x)))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.2.1.1.1.1.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_17) = {2}
Following symbols are considered usable:
{if_replace,replace,eq#,if_min#,if_replace#,le#,min#,replace#,sort#}
TcT has computed the following interpretation:
p(0) = [2]
p(cons) = [1] x1 + [1] x2 + [1]
p(eq) = [4] x1 + [1]
p(false) = [3]
p(if_min) = [4] x1 + [1] x2 + [1]
p(if_replace) = [1] x3 + [1] x4 + [0]
p(le) = [3] x1 + [2]
p(min) = [2] x1 + [0]
p(nil) = [0]
p(replace) = [1] x2 + [1] x3 + [0]
p(s) = [2]
p(sort) = [1]
p(true) = [0]
p(eq#) = [2]
p(if_min#) = [1]
p(if_replace#) = [2] x1 + [1] x3 + [1] x4 + [1]
p(le#) = [4] x1 + [1] x2 + [0]
p(min#) = [4] x1 + [4]
p(replace#) = [0]
p(sort#) = [4] x1 + [1]
p(c_1) = [0]
p(c_2) = [0]
p(c_3) = [0]
p(c_4) = [1]
p(c_5) = [1]
p(c_6) = [1] x1 + [0]
p(c_7) = [4]
p(c_8) = [1]
p(c_9) = [4]
p(c_10) = [0]
p(c_11) = [1] x1 + [1]
p(c_12) = [4] x1 + [1]
p(c_13) = [0]
p(c_14) = [0]
p(c_15) = [1] x1 + [0]
p(c_16) = [1]
p(c_17) = [1] x2 + [1]
p(c_18) = [0]
Following rules are strictly oriented:
sort#(cons(n,x)) = [4] n + [4] x + [5]
> [4] n + [4] x + [2]
= c_17(min#(cons(n,x))
,sort#(replace(min(cons(n,x))
,n
,x))
,min#(cons(n,x)))
Following rules are (at-least) weakly oriented:
if_replace(false() = [1] k + [1] m + [1] x + [1]
,n
,m
,cons(k,x))
>= [1] k + [1] m + [1] x + [1]
= cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) = [1] k + [1] m + [1] x + [1]
>= [1] m + [1] x + [1]
= cons(m,x)
replace(n,m,cons(k,x)) = [1] k + [1] m + [1] x + [1]
>= [1] k + [1] m + [1] x + [1]
= if_replace(eq(n,k)
,n
,m
,cons(k,x))
replace(n,m,nil()) = [1] m + [0]
>= [0]
= nil()
*** 1.1.1.1.1.2.1.1.1.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),min#(cons(n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.1.1.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),min#(cons(n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),min#(cons(n,x)))
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),min#(cons(n,x))):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: sort#(cons(n,x)) ->
c_17(min#(cons(n,x))
,sort#(replace(min(cons(n,x))
,n
,x))
,min#(cons(n,x)))
*** 1.1.1.1.1.2.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:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.2.1.1.1.1.1.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
3: le#(s(n),s(m)) -> c_11(le#(n,m))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.2.1.1.1.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima):
The following argument positions are considered usable:
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_11) = {1},
uargs(c_12) = {1,2}
Following symbols are considered usable:
{if_replace,replace,eq#,if_min#,if_replace#,le#,min#,replace#,sort#}
TcT has computed the following interpretation:
p(0) = [1]
[0]
[1]
p(cons) = [0 0 0] [0 1 0] [0]
[0 0 0] x1 + [0 0 1] x2 + [0]
[0 0 1] [0 0 1] [0]
p(eq) = [0]
[0]
[1]
p(false) = [0]
[0]
[0]
p(if_min) = [0]
[0]
[1]
p(if_replace) = [0 0 1] [1 1 0] [0]
[0 0 1] x3 + [0 1 0] x4 + [0]
[0 0 1] [0 0 1] [0]
p(le) = [1 1 0] [0 0 1] [1]
[0 0 1] x1 + [1 0 0] x2 + [1]
[0 0 0] [0 0 0] [0]
p(min) = [1 1 0] [0]
[0 0 0] x1 + [0]
[0 0 0] [0]
p(nil) = [0]
[0]
[0]
p(replace) = [0 0 1] [1 0 1] [0]
[0 0 1] x2 + [0 0 1] x3 + [0]
[0 0 1] [0 0 1] [0]
p(s) = [0 0 0] [1]
[0 0 1] x1 + [0]
[0 0 1] [1]
p(sort) = [0]
[0]
[0]
p(true) = [0]
[0]
[0]
p(eq#) = [0]
[0]
[0]
p(if_min#) = [1 0 0] [0]
[0 1 1] x2 + [0]
[0 0 0] [1]
p(if_replace#) = [0]
[0]
[0]
p(le#) = [0 0 1] [0]
[0 0 1] x2 + [0]
[1 0 0] [0]
p(min#) = [0 1 0] [0]
[0 0 0] x1 + [0]
[0 0 0] [1]
p(replace#) = [0]
[0]
[0]
p(sort#) = [0 0 1] [1]
[0 0 0] x1 + [0]
[0 0 0] [1]
p(c_1) = [0]
[0]
[0]
p(c_2) = [0]
[0]
[0]
p(c_3) = [0]
[0]
[0]
p(c_4) = [0]
[0]
[0]
p(c_5) = [1 0 0] [0]
[0 0 0] x1 + [0]
[0 0 0] [1]
p(c_6) = [1 0 0] [0]
[0 0 0] x1 + [0]
[0 0 1] [0]
p(c_7) = [0]
[0]
[0]
p(c_8) = [0]
[0]
[0]
p(c_9) = [0]
[0]
[0]
p(c_10) = [0]
[0]
[0]
p(c_11) = [1 0 0] [0]
[0 0 0] x1 + [0]
[0 0 0] [1]
p(c_12) = [1 0 0] [1 0 0] [0]
[0 0 0] x1 + [0 0 0] x2 + [0]
[0 0 0] [0 0 0] [0]
p(c_13) = [0]
[0]
[0]
p(c_14) = [0]
[0]
[0]
p(c_15) = [0]
[0]
[0]
p(c_16) = [0]
[0]
[0]
p(c_17) = [0]
[0]
[0]
p(c_18) = [0]
[0]
[0]
Following rules are strictly oriented:
le#(s(n),s(m)) = [0 0 1] [1]
[0 0 1] m + [1]
[0 0 0] [1]
> [0 0 1] [0]
[0 0 0] m + [0]
[0 0 0] [1]
= c_11(le#(n,m))
Following rules are (at-least) weakly oriented:
if_min#(false() = [0 0 0] [0 0 0] [0 0
,cons(n,cons(m,x))) 1] [0]
[0 0 2] m + [0 0 1] n + [0 0
2] x + [0]
[0 0 0] [0 0 0] [0 0
0] [1]
>= [0 0 1] [0]
[0 0 0] x + [0]
[0 0 0] [1]
= c_5(min#(cons(m,x)))
if_min#(true() = [0 0 0] [0 0 0] [0 0
,cons(n,cons(m,x))) 1] [0]
[0 0 2] m + [0 0 1] n + [0 0
2] x + [0]
[0 0 0] [0 0 0] [0 0
0] [1]
>= [0 0 1] [0]
[0 0 0] x + [0]
[0 0 0] [1]
= c_6(min#(cons(n,x)))
min#(cons(n,cons(m,x))) = [0 0 1] [0 0 1] [0]
[0 0 0] m + [0 0 0] x + [0]
[0 0 0] [0 0 0] [1]
>= [0 0 1] [0 0 1] [0]
[0 0 0] m + [0 0 0] x + [0]
[0 0 0] [0 0 0] [0]
= c_12(if_min#(le(n,m)
,cons(n,cons(m,x)))
,le#(n,m))
sort#(cons(n,x)) = [0 0 1] [0 0 1] [1]
[0 0 0] n + [0 0 0] x + [0]
[0 0 0] [0 0 0] [1]
>= [0 0 1] [0]
[0 0 0] x + [0]
[0 0 0] [1]
= min#(cons(n,x))
sort#(cons(n,x)) = [0 0 1] [0 0 1] [1]
[0 0 0] n + [0 0 0] x + [0]
[0 0 0] [0 0 0] [1]
>= [0 0 1] [0 0 1] [1]
[0 0 0] n + [0 0 0] x + [0]
[0 0 0] [0 0 0] [1]
= sort#(replace(min(cons(n,x))
,n
,x))
if_replace(false() = [0 0 0] [0 0 1] [0 1
,n 1] [0]
,m [0 0 0] k + [0 0 1] m + [0 0
,cons(k,x)) 1] x + [0]
[0 0 1] [0 0 1] [0 0
1] [0]
>= [0 0 0] [0 0 1] [0 0
1] [0]
[0 0 0] k + [0 0 1] m + [0 0
1] x + [0]
[0 0 1] [0 0 1] [0 0
1] [0]
= cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) = [0 0 0] [0 0 1] [0 1
1] [0]
[0 0 0] k + [0 0 1] m + [0 0
1] x + [0]
[0 0 1] [0 0 1] [0 0
1] [0]
>= [0 0 0] [0 1 0] [0]
[0 0 0] m + [0 0 1] x + [0]
[0 0 1] [0 0 1] [0]
= cons(m,x)
replace(n,m,cons(k,x)) = [0 0 1] [0 0 1] [0 1
1] [0]
[0 0 1] k + [0 0 1] m + [0 0
1] x + [0]
[0 0 1] [0 0 1] [0 0
1] [0]
>= [0 0 0] [0 0 1] [0 1
1] [0]
[0 0 0] k + [0 0 1] m + [0 0
1] x + [0]
[0 0 1] [0 0 1] [0 0
1] [0]
= if_replace(eq(n,k)
,n
,m
,cons(k,x))
replace(n,m,nil()) = [0 0 1] [0]
[0 0 1] m + [0]
[0 0 1] [0]
>= [0]
[0]
[0]
= nil()
*** 1.1.1.1.1.2.1.1.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Strict TRS Rules:
Weak DP Rules:
le#(s(n),s(m)) -> c_11(le#(n,m))
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.1.1.1.2.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Strict TRS Rules:
Weak DP Rules:
le#(s(n),s(m)) -> c_11(le#(n,m))
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):3
2:S:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):3
3:S:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
-->_2 le#(s(n),s(m)) -> c_11(le#(n,m)):4
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):2
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):1
4:W:le#(s(n),s(m)) -> c_11(le#(n,m))
-->_1 le#(s(n),s(m)) -> c_11(le#(n,m)):4
5:W:sort#(cons(n,x)) -> min#(cons(n,x))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):3
6:W:sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
-->_1 sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x)):6
-->_1 sort#(cons(n,x)) -> min#(cons(n,x)):5
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
4: le#(s(n),s(m)) -> c_11(le#(n,m))
*** 1.1.1.1.1.2.1.1.1.1.1.2.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):3
2:S:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):3
3:S:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):2
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):1
5:W:sort#(cons(n,x)) -> min#(cons(n,x))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):3
6:W:sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
-->_1 sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x)):6
-->_1 sort#(cons(n,x)) -> min#(cons(n,x)):5
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))))
*** 1.1.1.1.1.2.1.1.1.1.1.2.2.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: if_min#(false()
,cons(n,cons(m,x))) ->
c_5(min#(cons(m,x)))
2: if_min#(true()
,cons(n,cons(m,x))) ->
c_6(min#(cons(n,x)))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.2.1.1.1.1.1.2.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_12) = {1}
Following symbols are considered usable:
{eq,if_replace,replace,eq#,if_min#,if_replace#,le#,min#,replace#,sort#}
TcT has computed the following interpretation:
p(0) = [0]
p(cons) = [1] x2 + [1]
p(eq) = [1] x1 + [0]
p(false) = [0]
p(if_min) = [0]
p(if_replace) = [1] x4 + [1]
p(le) = [0]
p(min) = [2] x1 + [2]
p(nil) = [5]
p(replace) = [1] x3 + [1]
p(s) = [1] x1 + [4]
p(sort) = [1] x1 + [0]
p(true) = [0]
p(eq#) = [2] x2 + [0]
p(if_min#) = [1] x2 + [0]
p(if_replace#) = [1] x1 + [1] x3 + [0]
p(le#) = [1] x1 + [2] x2 + [4]
p(min#) = [1] x1 + [0]
p(replace#) = [2] x3 + [1]
p(sort#) = [1] x1 + [1]
p(c_1) = [1]
p(c_2) = [0]
p(c_3) = [0]
p(c_4) = [1]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [0]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [1]
p(c_10) = [1]
p(c_11) = [0]
p(c_12) = [1] x1 + [0]
p(c_13) = [0]
p(c_14) = [1]
p(c_15) = [0]
p(c_16) = [0]
p(c_17) = [4] x1 + [1] x2 + [1]
p(c_18) = [0]
Following rules are strictly oriented:
if_min#(false() = [1] x + [2]
,cons(n,cons(m,x)))
> [1] x + [1]
= c_5(min#(cons(m,x)))
if_min#(true() = [1] x + [2]
,cons(n,cons(m,x)))
> [1] x + [1]
= c_6(min#(cons(n,x)))
Following rules are (at-least) weakly oriented:
min#(cons(n,cons(m,x))) = [1] x + [2]
>= [1] x + [2]
= c_12(if_min#(le(n,m)
,cons(n,cons(m,x))))
sort#(cons(n,x)) = [1] x + [2]
>= [1] x + [1]
= min#(cons(n,x))
sort#(cons(n,x)) = [1] x + [2]
>= [1] x + [2]
= sort#(replace(min(cons(n,x))
,n
,x))
eq(0(),0()) = [0]
>= [0]
= true()
eq(0(),s(m)) = [0]
>= [0]
= false()
eq(s(n),0()) = [1] n + [4]
>= [0]
= false()
eq(s(n),s(m)) = [1] n + [4]
>= [1] n + [0]
= eq(n,m)
if_replace(false() = [1] x + [2]
,n
,m
,cons(k,x))
>= [1] x + [2]
= cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) = [1] x + [2]
>= [1] x + [1]
= cons(m,x)
replace(n,m,cons(k,x)) = [1] x + [2]
>= [1] x + [2]
= if_replace(eq(n,k)
,n
,m
,cons(k,x))
replace(n,m,nil()) = [6]
>= [5]
= nil()
*** 1.1.1.1.1.2.1.1.1.1.1.2.2.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))))
Strict TRS Rules:
Weak DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.1.1.1.2.2.1.1.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))))
Strict TRS Rules:
Weak DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: min#(cons(n,cons(m,x))) ->
c_12(if_min#(le(n,m)
,cons(n,cons(m,x))))
Consider the set of all dependency pairs
1: min#(cons(n,cons(m,x))) ->
c_12(if_min#(le(n,m)
,cons(n,cons(m,x))))
2: if_min#(false()
,cons(n,cons(m,x))) ->
c_5(min#(cons(m,x)))
3: if_min#(true()
,cons(n,cons(m,x))) ->
c_6(min#(cons(n,x)))
4: sort#(cons(n,x)) -> min#(cons(n
,x))
5: sort#(cons(n,x)) ->
sort#(replace(min(cons(n,x))
,n
,x))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,2,3}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.2.1.1.1.1.1.2.2.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))))
Strict TRS Rules:
Weak DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_5) = {1},
uargs(c_6) = {1},
uargs(c_12) = {1}
Following symbols are considered usable:
{if_min,if_replace,min,replace,eq#,if_min#,if_replace#,le#,min#,replace#,sort#}
TcT has computed the following interpretation:
p(0) = [0]
p(cons) = [1] x2 + [2]
p(eq) = [2]
p(false) = [0]
p(if_min) = [1]
p(if_replace) = [1] x2 + [1] x4 + [1]
p(le) = [0]
p(min) = [1]
p(nil) = [4]
p(replace) = [1] x1 + [1] x3 + [1]
p(s) = [0]
p(sort) = [0]
p(true) = [0]
p(eq#) = [2] x2 + [1]
p(if_min#) = [2] x2 + [6]
p(if_replace#) = [1] x1 + [1] x3 + [1] x4 + [2]
p(le#) = [1] x1 + [4] x2 + [1]
p(min#) = [2] x1 + [7]
p(replace#) = [1] x3 + [0]
p(sort#) = [4] x1 + [3]
p(c_1) = [1]
p(c_2) = [2]
p(c_3) = [1]
p(c_4) = [0]
p(c_5) = [1] x1 + [0]
p(c_6) = [1] x1 + [2]
p(c_7) = [4]
p(c_8) = [1]
p(c_9) = [1]
p(c_10) = [0]
p(c_11) = [4]
p(c_12) = [1] x1 + [0]
p(c_13) = [1]
p(c_14) = [1]
p(c_15) = [1] x1 + [1]
p(c_16) = [1]
p(c_17) = [1] x2 + [0]
p(c_18) = [0]
Following rules are strictly oriented:
min#(cons(n,cons(m,x))) = [2] x + [15]
> [2] x + [14]
= c_12(if_min#(le(n,m)
,cons(n,cons(m,x))))
Following rules are (at-least) weakly oriented:
if_min#(false() = [2] x + [14]
,cons(n,cons(m,x)))
>= [2] x + [11]
= c_5(min#(cons(m,x)))
if_min#(true() = [2] x + [14]
,cons(n,cons(m,x)))
>= [2] x + [13]
= c_6(min#(cons(n,x)))
sort#(cons(n,x)) = [4] x + [11]
>= [2] x + [11]
= min#(cons(n,x))
sort#(cons(n,x)) = [4] x + [11]
>= [4] x + [11]
= sort#(replace(min(cons(n,x))
,n
,x))
if_min(false() = [1]
,cons(n,cons(m,x)))
>= [1]
= min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) = [1]
>= [1]
= min(cons(n,x))
if_replace(false() = [1] n + [1] x + [3]
,n
,m
,cons(k,x))
>= [1] n + [1] x + [3]
= cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) = [1] n + [1] x + [3]
>= [1] x + [2]
= cons(m,x)
min(cons(n,cons(m,x))) = [1]
>= [1]
= if_min(le(n,m)
,cons(n,cons(m,x)))
min(cons(0(),nil())) = [1]
>= [0]
= 0()
min(cons(s(n),nil())) = [1]
>= [0]
= s(n)
replace(n,m,cons(k,x)) = [1] n + [1] x + [3]
>= [1] n + [1] x + [3]
= if_replace(eq(n,k)
,n
,m
,cons(k,x))
replace(n,m,nil()) = [1] n + [5]
>= [4]
= nil()
*** 1.1.1.1.1.2.1.1.1.1.1.2.2.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))))
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.1.1.1.2.2.1.1.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))))
sort#(cons(n,x)) -> min#(cons(n,x))
sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x)))):3
2:W:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x)))):3
3:W:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))))
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):2
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):1
4:W:sort#(cons(n,x)) -> min#(cons(n,x))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x)))):3
5:W:sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x))
-->_1 sort#(cons(n,x)) -> sort#(replace(min(cons(n,x)),n,x)):5
-->_1 sort#(cons(n,x)) -> min#(cons(n,x)):4
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
5: sort#(cons(n,x)) ->
sort#(replace(min(cons(n,x))
,n
,x))
4: sort#(cons(n,x)) -> min#(cons(n
,x))
1: if_min#(false()
,cons(n,cons(m,x))) ->
c_5(min#(cons(m,x)))
3: min#(cons(n,cons(m,x))) ->
c_12(if_min#(le(n,m)
,cons(n,cons(m,x))))
2: if_min#(true()
,cons(n,cons(m,x))) ->
c_6(min#(cons(n,x)))
*** 1.1.1.1.1.2.1.1.1.1.1.2.2.1.1.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/1,c_13/0,c_14/0,c_15/1,c_16/0,c_17/3,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.2.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
le#(s(n),s(m)) -> c_11(le#(n,m))
min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):2
2:S:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):1
3:S:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
-->_4 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):7
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):7
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x))):3
-->_3 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):2
4:W:if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):7
5:W:if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x)))
-->_1 min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m)):7
6:W:le#(s(n),s(m)) -> c_11(le#(n,m))
-->_1 le#(s(n),s(m)) -> c_11(le#(n,m)):6
7:W:min#(cons(n,cons(m,x))) -> c_12(if_min#(le(n,m),cons(n,cons(m,x))),le#(n,m))
-->_2 le#(s(n),s(m)) -> c_11(le#(n,m)):6
-->_1 if_min#(true(),cons(n,cons(m,x))) -> c_6(min#(cons(n,x))):5
-->_1 if_min#(false(),cons(n,cons(m,x))) -> c_5(min#(cons(m,x))):4
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
7: min#(cons(n,cons(m,x))) ->
c_12(if_min#(le(n,m)
,cons(n,cons(m,x)))
,le#(n,m))
5: if_min#(true()
,cons(n,cons(m,x))) ->
c_6(min#(cons(n,x)))
4: if_min#(false()
,cons(n,cons(m,x))) ->
c_5(min#(cons(m,x)))
6: le#(s(n),s(m)) -> c_11(le#(n,m))
*** 1.1.1.1.1.2.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/4,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):2
2:S:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):1
3:S:sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x)))
-->_2 sort#(cons(n,x)) -> c_17(min#(cons(n,x)),sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x),min#(cons(n,x))):3
-->_3 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):2
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
*** 1.1.1.1.1.2.1.1.2.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
Proof:
We analyse the complexity of following sub-problems (R) and (S).
Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component.
Problem (R)
Strict DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Problem (S)
Strict DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
*** 1.1.1.1.1.2.1.1.2.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: if_replace#(false()
,n
,m
,cons(k,x)) -> c_7(replace#(n
,m
,x))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.2.1.1.2.1.1.1.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_7) = {1},
uargs(c_15) = {1},
uargs(c_17) = {1,2}
Following symbols are considered usable:
{if_replace,replace,eq#,if_min#,if_replace#,le#,min#,replace#,sort#}
TcT has computed the following interpretation:
p(0) = [1]
[2]
p(cons) = [1 3] x2 + [0]
[0 1] [1]
p(eq) = [1 3] x1 + [0]
[0 0] [0]
p(false) = [0]
[0]
p(if_min) = [0 2] x1 + [1]
[2 0] [2]
p(if_replace) = [1 0] x4 + [0]
[0 1] [0]
p(le) = [1 0] x1 + [2 0] x2 + [1]
[2 2] [0 0] [0]
p(min) = [0]
[0]
p(nil) = [0]
[0]
p(replace) = [1 0] x3 + [0]
[0 1] [0]
p(s) = [0 2] x1 + [0]
[0 1] [0]
p(sort) = [2]
[0]
p(true) = [0]
[0]
p(eq#) = [2]
[2]
p(if_min#) = [0]
[0]
p(if_replace#) = [0 0] x2 + [0 0] x3 + [0
1] x4 + [0]
[0 2] [0 2] [0
3] [2]
p(le#) = [1 0] x1 + [2 1] x2 + [0]
[2 0] [0 0] [0]
p(min#) = [0 0] x1 + [0]
[0 1] [1]
p(replace#) = [0 1] x3 + [0]
[0 0] [1]
p(sort#) = [1 1] x1 + [0]
[0 0] [2]
p(c_1) = [0]
[1]
p(c_2) = [0]
[2]
p(c_3) = [1]
[0]
p(c_4) = [0 0] x1 + [2]
[1 2] [2]
p(c_5) = [0 1] x1 + [0]
[0 0] [2]
p(c_6) = [0 2] x1 + [2]
[0 1] [2]
p(c_7) = [1 0] x1 + [0]
[0 0] [1]
p(c_8) = [0]
[0]
p(c_9) = [0]
[0]
p(c_10) = [2]
[0]
p(c_11) = [0 0] x1 + [0]
[0 1] [0]
p(c_12) = [0 0] x1 + [0]
[1 2] [0]
p(c_13) = [0]
[0]
p(c_14) = [1]
[0]
p(c_15) = [1 0] x1 + [0]
[0 0] [0]
p(c_16) = [2]
[1]
p(c_17) = [1 0] x1 + [2 0] x2 + [0]
[0 0] [0 1] [0]
p(c_18) = [1]
[2]
Following rules are strictly oriented:
if_replace#(false() = [0 0] m + [0 0] n + [0
,n 1] x + [1]
,m [0 2] [0 2] [0
,cons(k,x)) 3] [5]
> [0 1] x + [0]
[0 0] [1]
= c_7(replace#(n,m,x))
Following rules are (at-least) weakly oriented:
replace#(n,m,cons(k,x)) = [0 1] x + [1]
[0 0] [1]
>= [0 1] x + [1]
[0 0] [0]
= c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x)))
sort#(cons(n,x)) = [1 4] x + [1]
[0 0] [2]
>= [1 3] x + [0]
[0 0] [1]
= c_17(sort#(replace(min(cons(n
,x))
,n
,x))
,replace#(min(cons(n,x)),n,x))
if_replace(false() = [1 3] x + [0]
,n [0 1] [1]
,m
,cons(k,x))
>= [1 3] x + [0]
[0 1] [1]
= cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) = [1 3] x + [0]
[0 1] [1]
>= [1 3] x + [0]
[0 1] [1]
= cons(m,x)
replace(n,m,cons(k,x)) = [1 3] x + [0]
[0 1] [1]
>= [1 3] x + [0]
[0 1] [1]
= if_replace(eq(n,k)
,n
,m
,cons(k,x))
replace(n,m,nil()) = [0]
[0]
>= [0]
[0]
= nil()
*** 1.1.1.1.1.2.1.1.2.1.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.2.1.1.1.2 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: replace#(n,m,cons(k,x)) ->
c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x)))
Consider the set of all dependency pairs
1: replace#(n,m,cons(k,x)) ->
c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x)))
2: if_replace#(false()
,n
,m
,cons(k,x)) -> c_7(replace#(n
,m
,x))
3: sort#(cons(n,x)) ->
c_17(sort#(replace(min(cons(n
,x))
,n
,x))
,replace#(min(cons(n,x)),n,x))
Processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, 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,2}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
*** 1.1.1.1.1.2.1.1.2.1.1.1.2.1 Progress [(?,O(n^2))] ***
Considered Problem:
Strict DP Rules:
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_7) = {1},
uargs(c_15) = {1},
uargs(c_17) = {1,2}
Following symbols are considered usable:
{if_replace,replace,eq#,if_min#,if_replace#,le#,min#,replace#,sort#}
TcT has computed the following interpretation:
p(0) = [0]
[0]
p(cons) = [1 2] x2 + [1]
[0 1] [1]
p(eq) = [0]
[0]
p(false) = [0]
[0]
p(if_min) = [0 0] x1 + [0 1] x2 + [2]
[1 1] [0 0] [0]
p(if_replace) = [1 0] x4 + [0]
[0 1] [0]
p(le) = [1 1] x1 + [0 0] x2 + [1]
[0 0] [0 1] [2]
p(min) = [0 0] x1 + [1]
[0 1] [0]
p(nil) = [1]
[2]
p(replace) = [1 0] x3 + [0]
[0 1] [0]
p(s) = [3]
[2]
p(sort) = [2]
[0]
p(true) = [1]
[3]
p(eq#) = [0 0] x2 + [0]
[1 1] [2]
p(if_min#) = [0]
[0]
p(if_replace#) = [0 0] x2 + [0 1] x4 + [0]
[0 2] [1 0] [1]
p(le#) = [0 0] x1 + [0 0] x2 + [2]
[1 0] [2 0] [1]
p(min#) = [0]
[2]
p(replace#) = [0 1] x3 + [1]
[0 2] [0]
p(sort#) = [2 0] x1 + [1]
[0 0] [1]
p(c_1) = [0]
[0]
p(c_2) = [0]
[0]
p(c_3) = [2]
[0]
p(c_4) = [0]
[2]
p(c_5) = [1]
[1]
p(c_6) = [0]
[0]
p(c_7) = [1 0] x1 + [0]
[0 1] [0]
p(c_8) = [0]
[0]
p(c_9) = [1]
[0]
p(c_10) = [2]
[0]
p(c_11) = [1 0] x1 + [1]
[0 1] [0]
p(c_12) = [0 0] x2 + [0]
[2 2] [2]
p(c_13) = [2]
[0]
p(c_14) = [0]
[0]
p(c_15) = [1 0] x1 + [0]
[1 0] [0]
p(c_16) = [0]
[0]
p(c_17) = [1 1] x1 + [1 1] x2 + [0]
[0 0] [0 0] [1]
p(c_18) = [1]
[0]
Following rules are strictly oriented:
replace#(n,m,cons(k,x)) = [0 1] x + [2]
[0 2] [2]
> [0 1] x + [1]
[0 1] [1]
= c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x)))
Following rules are (at-least) weakly oriented:
if_replace#(false() = [0 0] n + [0 1] x + [1]
,n [0 2] [1 2] [2]
,m
,cons(k,x))
>= [0 1] x + [1]
[0 2] [0]
= c_7(replace#(n,m,x))
sort#(cons(n,x)) = [2 4] x + [3]
[0 0] [1]
>= [2 3] x + [3]
[0 0] [1]
= c_17(sort#(replace(min(cons(n
,x))
,n
,x))
,replace#(min(cons(n,x)),n,x))
if_replace(false() = [1 2] x + [1]
,n [0 1] [1]
,m
,cons(k,x))
>= [1 2] x + [1]
[0 1] [1]
= cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) = [1 2] x + [1]
[0 1] [1]
>= [1 2] x + [1]
[0 1] [1]
= cons(m,x)
replace(n,m,cons(k,x)) = [1 2] x + [1]
[0 1] [1]
>= [1 2] x + [1]
[0 1] [1]
= if_replace(eq(n,k)
,n
,m
,cons(k,x))
replace(n,m,nil()) = [1]
[2]
>= [1]
[2]
= nil()
*** 1.1.1.1.1.2.1.1.2.1.1.1.2.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.2.1.1.1.2.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):2
2:W:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):1
3:W:sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
-->_1 sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x)):3
-->_2 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: sort#(cons(n,x)) ->
c_17(sort#(replace(min(cons(n
,x))
,n
,x))
,replace#(min(cons(n,x)),n,x))
1: if_replace#(false()
,n
,m
,cons(k,x)) -> c_7(replace#(n
,m
,x))
2: replace#(n,m,cons(k,x)) ->
c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x)))
*** 1.1.1.1.1.2.1.1.2.1.1.1.2.2.1 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).
*** 1.1.1.1.1.2.1.1.2.1.1.2 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Strict TRS Rules:
Weak DP Rules:
if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:S:sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
-->_2 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):3
-->_1 sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x)):1
2:W:if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x))
-->_1 replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x))):3
3:W:replace#(n,m,cons(k,x)) -> c_15(if_replace#(eq(n,k),n,m,cons(k,x)))
-->_1 if_replace#(false(),n,m,cons(k,x)) -> c_7(replace#(n,m,x)):2
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: replace#(n,m,cons(k,x)) ->
c_15(if_replace#(eq(n,k)
,n
,m
,cons(k,x)))
2: if_replace#(false()
,n
,m
,cons(k,x)) -> c_7(replace#(n
,m
,x))
*** 1.1.1.1.1.2.1.1.2.1.1.2.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/2,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
SimplifyRHS
Proof:
Consider the dependency graph
1:S:sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x))
-->_1 sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)),replace#(min(cons(n,x)),n,x)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)))
*** 1.1.1.1.1.2.1.1.2.1.1.2.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy}}
Proof:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing, greedy = NoGreedy} to orient following rules strictly:
1: sort#(cons(n,x)) ->
c_17(sort#(replace(min(cons(n
,x))
,n
,x)))
The strictly oriented rules are moved into the weak component.
*** 1.1.1.1.1.2.1.1.2.1.1.2.1.1.1 Progress [(?,O(n^1))] ***
Considered Problem:
Strict DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)))
Strict TRS Rules:
Weak DP Rules:
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation any intersect of rules of CDG leaf and strict-rules, greedy = NoGreedy}
Proof:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_17) = {1}
Following symbols are considered usable:
{if_replace,replace,eq#,if_min#,if_replace#,le#,min#,replace#,sort#}
TcT has computed the following interpretation:
p(0) = [0]
p(cons) = [1] x2 + [4]
p(eq) = [0]
p(false) = [0]
p(if_min) = [4] x1 + [0]
p(if_replace) = [1] x4 + [0]
p(le) = [2] x1 + [2] x2 + [0]
p(min) = [1]
p(nil) = [4]
p(replace) = [1] x3 + [0]
p(s) = [1]
p(sort) = [1] x1 + [1]
p(true) = [0]
p(eq#) = [0]
p(if_min#) = [1] x1 + [1]
p(if_replace#) = [1] x2 + [1] x3 + [1] x4 + [0]
p(le#) = [1] x1 + [1] x2 + [1]
p(min#) = [2] x1 + [1]
p(replace#) = [2]
p(sort#) = [2] x1 + [1]
p(c_1) = [1]
p(c_2) = [1]
p(c_3) = [0]
p(c_4) = [4] x1 + [1]
p(c_5) = [0]
p(c_6) = [2] x1 + [1]
p(c_7) = [4] x1 + [1]
p(c_8) = [2]
p(c_9) = [1]
p(c_10) = [2]
p(c_11) = [0]
p(c_12) = [0]
p(c_13) = [4]
p(c_14) = [1]
p(c_15) = [2]
p(c_16) = [4]
p(c_17) = [1] x1 + [6]
p(c_18) = [1]
Following rules are strictly oriented:
sort#(cons(n,x)) = [2] x + [9]
> [2] x + [7]
= c_17(sort#(replace(min(cons(n
,x))
,n
,x)))
Following rules are (at-least) weakly oriented:
if_replace(false() = [1] x + [4]
,n
,m
,cons(k,x))
>= [1] x + [4]
= cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) = [1] x + [4]
>= [1] x + [4]
= cons(m,x)
replace(n,m,cons(k,x)) = [1] x + [4]
>= [1] x + [4]
= if_replace(eq(n,k)
,n
,m
,cons(k,x))
replace(n,m,nil()) = [4]
>= [4]
= nil()
*** 1.1.1.1.1.2.1.1.2.1.1.2.1.1.1.1 Progress [(?,O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
Assumption
Proof:
()
*** 1.1.1.1.1.2.1.1.2.1.1.2.1.1.2 Progress [(O(1),O(1))] ***
Considered Problem:
Strict DP Rules:
Strict TRS Rules:
Weak DP Rules:
sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)))
Weak TRS Rules:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
RemoveWeakSuffixes
Proof:
Consider the dependency graph
1:W:sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x)))
-->_1 sort#(cons(n,x)) -> c_17(sort#(replace(min(cons(n,x)),n,x))):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: sort#(cons(n,x)) ->
c_17(sort#(replace(min(cons(n
,x))
,n
,x)))
*** 1.1.1.1.1.2.1.1.2.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:
eq(0(),0()) -> true()
eq(0(),s(m)) -> false()
eq(s(n),0()) -> false()
eq(s(n),s(m)) -> eq(n,m)
if_min(false(),cons(n,cons(m,x))) -> min(cons(m,x))
if_min(true(),cons(n,cons(m,x))) -> min(cons(n,x))
if_replace(false(),n,m,cons(k,x)) -> cons(k,replace(n,m,x))
if_replace(true(),n,m,cons(k,x)) -> cons(m,x)
le(0(),m) -> true()
le(s(n),0()) -> false()
le(s(n),s(m)) -> le(n,m)
min(cons(n,cons(m,x))) -> if_min(le(n,m),cons(n,cons(m,x)))
min(cons(0(),nil())) -> 0()
min(cons(s(n),nil())) -> s(n)
replace(n,m,cons(k,x)) -> if_replace(eq(n,k),n,m,cons(k,x))
replace(n,m,nil()) -> nil()
Signature:
{eq/2,if_min/2,if_replace/4,le/2,min/1,replace/3,sort/1,eq#/2,if_min#/2,if_replace#/4,le#/2,min#/1,replace#/3,sort#/1} / {0/0,cons/2,false/0,nil/0,s/1,true/0,c_1/0,c_2/0,c_3/0,c_4/1,c_5/1,c_6/1,c_7/1,c_8/0,c_9/0,c_10/0,c_11/1,c_12/2,c_13/0,c_14/0,c_15/1,c_16/0,c_17/1,c_18/0}
Obligation:
Innermost
basic terms: {eq#,if_min#,if_replace#,le#,min#,replace#,sort#}/{0,cons,false,nil,s,true}
Applied Processor:
EmptyProcessor
Proof:
The problem is already closed. The intended complexity is O(1).