WORST_CASE(?,O(n^3))
* Step 1: DependencyPairs WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
minSort(l) -> minSort#1(findMin(l))
minSort#1(dd(x,xs)) -> dd(x,minSort(xs))
minSort#1(nil()) -> nil()
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt,#compare,#less,findMin,findMin#1,findMin#2
,findMin#3,minSort,minSort#1} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
DependencyPairs {dpKind_ = DT}
+ Details:
We add the following dependency tuples:
Strict DPs
#cklt#(#EQ()) -> c_1()
#cklt#(#GT()) -> c_2()
#cklt#(#LT()) -> c_3()
#compare#(#0(),#0()) -> c_4()
#compare#(#0(),#neg(y)) -> c_5()
#compare#(#0(),#pos(y)) -> c_6()
#compare#(#0(),#s(y)) -> c_7()
#compare#(#neg(x),#0()) -> c_8()
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#neg(x),#pos(y)) -> c_10()
#compare#(#pos(x),#0()) -> c_11()
#compare#(#pos(x),#neg(y)) -> c_12()
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#0()) -> c_14()
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#1#(nil()) -> c_19()
findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y))
findMin#2#(nil(),x) -> c_21()
findMin#3#(#false(),x,y,ys) -> c_22()
findMin#3#(#true(),x,y,ys) -> c_23()
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
minSort#1#(nil()) -> c_26()
Weak DPs
and mark the set of starting terms.
* Step 2: UsableRules WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
#cklt#(#EQ()) -> c_1()
#cklt#(#GT()) -> c_2()
#cklt#(#LT()) -> c_3()
#compare#(#0(),#0()) -> c_4()
#compare#(#0(),#neg(y)) -> c_5()
#compare#(#0(),#pos(y)) -> c_6()
#compare#(#0(),#s(y)) -> c_7()
#compare#(#neg(x),#0()) -> c_8()
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#neg(x),#pos(y)) -> c_10()
#compare#(#pos(x),#0()) -> c_11()
#compare#(#pos(x),#neg(y)) -> c_12()
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#0()) -> c_14()
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#1#(nil()) -> c_19()
findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y))
findMin#2#(nil(),x) -> c_21()
findMin#3#(#false(),x,y,ys) -> c_22()
findMin#3#(#true(),x,y,ys) -> c_23()
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
minSort#1#(nil()) -> c_26()
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
minSort(l) -> minSort#1(findMin(l))
minSort#1(dd(x,xs)) -> dd(x,minSort(xs))
minSort#1(nil()) -> nil()
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
UsableRules
+ Details:
We replace rewrite rules by usable rules:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
#cklt#(#EQ()) -> c_1()
#cklt#(#GT()) -> c_2()
#cklt#(#LT()) -> c_3()
#compare#(#0(),#0()) -> c_4()
#compare#(#0(),#neg(y)) -> c_5()
#compare#(#0(),#pos(y)) -> c_6()
#compare#(#0(),#s(y)) -> c_7()
#compare#(#neg(x),#0()) -> c_8()
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#neg(x),#pos(y)) -> c_10()
#compare#(#pos(x),#0()) -> c_11()
#compare#(#pos(x),#neg(y)) -> c_12()
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#0()) -> c_14()
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#1#(nil()) -> c_19()
findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y))
findMin#2#(nil(),x) -> c_21()
findMin#3#(#false(),x,y,ys) -> c_22()
findMin#3#(#true(),x,y,ys) -> c_23()
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
minSort#1#(nil()) -> c_26()
* Step 3: PredecessorEstimation WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
#cklt#(#EQ()) -> c_1()
#cklt#(#GT()) -> c_2()
#cklt#(#LT()) -> c_3()
#compare#(#0(),#0()) -> c_4()
#compare#(#0(),#neg(y)) -> c_5()
#compare#(#0(),#pos(y)) -> c_6()
#compare#(#0(),#s(y)) -> c_7()
#compare#(#neg(x),#0()) -> c_8()
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#neg(x),#pos(y)) -> c_10()
#compare#(#pos(x),#0()) -> c_11()
#compare#(#pos(x),#neg(y)) -> c_12()
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#0()) -> c_14()
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#1#(nil()) -> c_19()
findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y))
findMin#2#(nil(),x) -> c_21()
findMin#3#(#false(),x,y,ys) -> c_22()
findMin#3#(#true(),x,y,ys) -> c_23()
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
minSort#1#(nil()) -> c_26()
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1,2,3,4,5,6,7,8,10,11,12,14,19,21,22,23,26}
by application of
Pre({1,2,3,4,5,6,7,8,10,11,12,14,19,21,22,23,26}) = {9,13,15,16,17,18,20,24}.
Here rules are labelled as follows:
1: #cklt#(#EQ()) -> c_1()
2: #cklt#(#GT()) -> c_2()
3: #cklt#(#LT()) -> c_3()
4: #compare#(#0(),#0()) -> c_4()
5: #compare#(#0(),#neg(y)) -> c_5()
6: #compare#(#0(),#pos(y)) -> c_6()
7: #compare#(#0(),#s(y)) -> c_7()
8: #compare#(#neg(x),#0()) -> c_8()
9: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
10: #compare#(#neg(x),#pos(y)) -> c_10()
11: #compare#(#pos(x),#0()) -> c_11()
12: #compare#(#pos(x),#neg(y)) -> c_12()
13: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
14: #compare#(#s(x),#0()) -> c_14()
15: #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
16: #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y))
17: findMin#(l) -> c_17(findMin#1#(l))
18: findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
19: findMin#1#(nil()) -> c_19()
20: findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y))
21: findMin#2#(nil(),x) -> c_21()
22: findMin#3#(#false(),x,y,ys) -> c_22()
23: findMin#3#(#true(),x,y,ys) -> c_23()
24: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
25: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
26: minSort#1#(nil()) -> c_26()
* Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak DPs:
#cklt#(#EQ()) -> c_1()
#cklt#(#GT()) -> c_2()
#cklt#(#LT()) -> c_3()
#compare#(#0(),#0()) -> c_4()
#compare#(#0(),#neg(y)) -> c_5()
#compare#(#0(),#pos(y)) -> c_6()
#compare#(#0(),#s(y)) -> c_7()
#compare#(#neg(x),#0()) -> c_8()
#compare#(#neg(x),#pos(y)) -> c_10()
#compare#(#pos(x),#0()) -> c_11()
#compare#(#pos(x),#neg(y)) -> c_12()
#compare#(#s(x),#0()) -> c_14()
findMin#1#(nil()) -> c_19()
findMin#2#(nil(),x) -> c_21()
findMin#3#(#false(),x,y,ys) -> c_22()
findMin#3#(#true(),x,y,ys) -> c_23()
minSort#1#(nil()) -> c_26()
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#s(x),#0()) -> c_14():21
-->_1 #compare#(#pos(x),#neg(y)) -> c_12():20
-->_1 #compare#(#pos(x),#0()) -> c_11():19
-->_1 #compare#(#neg(x),#pos(y)) -> c_10():18
-->_1 #compare#(#neg(x),#0()) -> c_8():17
-->_1 #compare#(#0(),#s(y)) -> c_7():16
-->_1 #compare#(#0(),#pos(y)) -> c_6():15
-->_1 #compare#(#0(),#neg(y)) -> c_5():14
-->_1 #compare#(#0(),#0()) -> c_4():13
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
2:S:#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#s(x),#0()) -> c_14():21
-->_1 #compare#(#pos(x),#neg(y)) -> c_12():20
-->_1 #compare#(#pos(x),#0()) -> c_11():19
-->_1 #compare#(#neg(x),#pos(y)) -> c_10():18
-->_1 #compare#(#neg(x),#0()) -> c_8():17
-->_1 #compare#(#0(),#s(y)) -> c_7():16
-->_1 #compare#(#0(),#pos(y)) -> c_6():15
-->_1 #compare#(#0(),#neg(y)) -> c_5():14
-->_1 #compare#(#0(),#0()) -> c_4():13
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
3:S:#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
-->_1 #compare#(#s(x),#0()) -> c_14():21
-->_1 #compare#(#pos(x),#neg(y)) -> c_12():20
-->_1 #compare#(#pos(x),#0()) -> c_11():19
-->_1 #compare#(#neg(x),#pos(y)) -> c_10():18
-->_1 #compare#(#neg(x),#0()) -> c_8():17
-->_1 #compare#(#0(),#s(y)) -> c_7():16
-->_1 #compare#(#0(),#pos(y)) -> c_6():15
-->_1 #compare#(#0(),#neg(y)) -> c_5():14
-->_1 #compare#(#0(),#0()) -> c_4():13
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
4:S:#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y))
-->_2 #compare#(#s(x),#0()) -> c_14():21
-->_2 #compare#(#pos(x),#neg(y)) -> c_12():20
-->_2 #compare#(#pos(x),#0()) -> c_11():19
-->_2 #compare#(#neg(x),#pos(y)) -> c_10():18
-->_2 #compare#(#neg(x),#0()) -> c_8():17
-->_2 #compare#(#0(),#s(y)) -> c_7():16
-->_2 #compare#(#0(),#pos(y)) -> c_6():15
-->_2 #compare#(#0(),#neg(y)) -> c_5():14
-->_2 #compare#(#0(),#0()) -> c_4():13
-->_1 #cklt#(#LT()) -> c_3():12
-->_1 #cklt#(#GT()) -> c_2():11
-->_1 #cklt#(#EQ()) -> c_1():10
-->_2 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_2 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_2 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
5:S:findMin#(l) -> c_17(findMin#1#(l))
-->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)):6
-->_1 findMin#1#(nil()) -> c_19():22
6:S:findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
-->_1 findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)):7
-->_1 findMin#2#(nil(),x) -> c_21():23
-->_2 findMin#(l) -> c_17(findMin#1#(l)):5
7:S:findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y))
-->_1 findMin#3#(#true(),x,y,ys) -> c_23():25
-->_1 findMin#3#(#false(),x,y,ys) -> c_22():24
-->_2 #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)):4
8:S:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
-->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):9
-->_1 minSort#1#(nil()) -> c_26():26
-->_2 findMin#(l) -> c_17(findMin#1#(l)):5
9:S:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
-->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):8
10:W:#cklt#(#EQ()) -> c_1()
11:W:#cklt#(#GT()) -> c_2()
12:W:#cklt#(#LT()) -> c_3()
13:W:#compare#(#0(),#0()) -> c_4()
14:W:#compare#(#0(),#neg(y)) -> c_5()
15:W:#compare#(#0(),#pos(y)) -> c_6()
16:W:#compare#(#0(),#s(y)) -> c_7()
17:W:#compare#(#neg(x),#0()) -> c_8()
18:W:#compare#(#neg(x),#pos(y)) -> c_10()
19:W:#compare#(#pos(x),#0()) -> c_11()
20:W:#compare#(#pos(x),#neg(y)) -> c_12()
21:W:#compare#(#s(x),#0()) -> c_14()
22:W:findMin#1#(nil()) -> c_19()
23:W:findMin#2#(nil(),x) -> c_21()
24:W:findMin#3#(#false(),x,y,ys) -> c_22()
25:W:findMin#3#(#true(),x,y,ys) -> c_23()
26:W:minSort#1#(nil()) -> c_26()
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
26: minSort#1#(nil()) -> c_26()
22: findMin#1#(nil()) -> c_19()
23: findMin#2#(nil(),x) -> c_21()
24: findMin#3#(#false(),x,y,ys) -> c_22()
25: findMin#3#(#true(),x,y,ys) -> c_23()
10: #cklt#(#EQ()) -> c_1()
11: #cklt#(#GT()) -> c_2()
12: #cklt#(#LT()) -> c_3()
13: #compare#(#0(),#0()) -> c_4()
14: #compare#(#0(),#neg(y)) -> c_5()
15: #compare#(#0(),#pos(y)) -> c_6()
16: #compare#(#0(),#s(y)) -> c_7()
17: #compare#(#neg(x),#0()) -> c_8()
18: #compare#(#neg(x),#pos(y)) -> c_10()
19: #compare#(#pos(x),#0()) -> c_11()
20: #compare#(#pos(x),#neg(y)) -> c_12()
21: #compare#(#s(x),#0()) -> c_14()
* Step 5: SimplifyRHS WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/2,c_17/1,c_18/2,c_19/0,c_20/2,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
2:S:#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
3:S:#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
4:S:#less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y))
-->_2 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_2 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_2 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
5:S:findMin#(l) -> c_17(findMin#1#(l))
-->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)):6
6:S:findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
-->_1 findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y)):7
-->_2 findMin#(l) -> c_17(findMin#1#(l)):5
7:S:findMin#2#(dd(y,ys),x) -> c_20(findMin#3#(#less(x,y),x,y,ys),#less#(x,y))
-->_2 #less#(x,y) -> c_16(#cklt#(#compare(x,y)),#compare#(x,y)):4
8:S:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
-->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):9
-->_2 findMin#(l) -> c_17(findMin#1#(l)):5
9:S:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
-->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):8
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
#less#(x,y) -> c_16(#compare#(x,y))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
* Step 6: Decompose WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
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 DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
- Weak DPs:
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0
,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0
,c_22/0,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
Problem (S)
- Strict DPs:
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0
,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0
,c_22/0,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
** Step 6.a:1: DecomposeDG WORST_CASE(?,O(n^3))
+ Considered Problem:
- Strict DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
- Weak DPs:
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing}
+ Details:
We decompose the input problem according to the dependency graph into the upper component
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
and a lower component
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
Further, following extension rules are added to the lower component.
minSort#(l) -> findMin#(l)
minSort#(l) -> minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) -> minSort#(xs)
*** Step 6.a:1.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
- Weak DPs:
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ 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}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
Consider the set of all dependency pairs
1: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
2: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}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}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
**** Step 6.a:1.a:1.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
- Weak DPs:
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_24) = {1},
uargs(c_25) = {1}
Following symbols are considered usable:
{#cklt,#less,findMin,findMin#1,findMin#2,findMin#3,#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#}
TcT has computed the following interpretation:
p(#0) = [2]
p(#EQ) = [0]
p(#GT) = [8]
p(#LT) = [4]
p(#cklt) = [1]
p(#compare) = [8] x1 + [4] x2 + [5]
p(#false) = [1]
p(#less) = [1]
p(#neg) = [0]
p(#pos) = [1] x1 + [2]
p(#s) = [1] x1 + [0]
p(#true) = [1]
p(dd) = [1] x2 + [8]
p(findMin) = [1] x1 + [0]
p(findMin#1) = [1] x1 + [0]
p(findMin#2) = [1] x1 + [8]
p(findMin#3) = [8] x1 + [1] x4 + [8]
p(minSort) = [2] x1 + [0]
p(minSort#1) = [1] x1 + [1]
p(nil) = [0]
p(#cklt#) = [1]
p(#compare#) = [8] x1 + [1] x2 + [1]
p(#less#) = [1] x1 + [0]
p(findMin#) = [1] x1 + [0]
p(findMin#1#) = [1] x1 + [1]
p(findMin#2#) = [1] x1 + [8] x2 + [1]
p(findMin#3#) = [2] x1 + [4] x4 + [0]
p(minSort#) = [2] x1 + [2]
p(minSort#1#) = [2] x1 + [0]
p(c_1) = [1]
p(c_2) = [2]
p(c_3) = [1]
p(c_4) = [0]
p(c_5) = [1]
p(c_6) = [1]
p(c_7) = [8]
p(c_8) = [1]
p(c_9) = [8]
p(c_10) = [0]
p(c_11) = [1]
p(c_12) = [8]
p(c_13) = [2]
p(c_14) = [0]
p(c_15) = [1] x1 + [2]
p(c_16) = [1] x1 + [1]
p(c_17) = [1]
p(c_18) = [1] x2 + [0]
p(c_19) = [1]
p(c_20) = [1] x1 + [0]
p(c_21) = [1]
p(c_22) = [1]
p(c_23) = [1]
p(c_24) = [1] x1 + [0]
p(c_25) = [1] x1 + [14]
p(c_26) = [1]
Following rules are strictly oriented:
minSort#(l) = [2] l + [2]
> [2] l + [0]
= c_24(minSort#1#(findMin(l)),findMin#(l))
Following rules are (at-least) weakly oriented:
minSort#1#(dd(x,xs)) = [2] xs + [16]
>= [2] xs + [16]
= c_25(minSort#(xs))
#cklt(#EQ()) = [1]
>= [1]
= #false()
#cklt(#GT()) = [1]
>= [1]
= #false()
#cklt(#LT()) = [1]
>= [1]
= #true()
#less(x,y) = [1]
>= [1]
= #cklt(#compare(x,y))
findMin(l) = [1] l + [0]
>= [1] l + [0]
= findMin#1(l)
findMin#1(dd(x,xs)) = [1] xs + [8]
>= [1] xs + [8]
= findMin#2(findMin(xs),x)
findMin#1(nil()) = [0]
>= [0]
= nil()
findMin#2(dd(y,ys),x) = [1] ys + [16]
>= [1] ys + [16]
= findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) = [8]
>= [8]
= dd(x,nil())
findMin#3(#false(),x,y,ys) = [1] ys + [16]
>= [1] ys + [16]
= dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) = [1] ys + [16]
>= [1] ys + [16]
= dd(x,dd(y,ys))
**** Step 6.a:1.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
**** Step 6.a:1.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
-->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):2
2:W:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
-->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
2: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
**** Step 6.a:1.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
*** Step 6.a:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
- Weak DPs:
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> findMin#(l)
minSort#(l) -> minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) -> minSort#(xs)
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ 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}}
+ Details:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
2: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
The strictly oriented rules are moved into the weak component.
**** Step 6.a:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
- Weak DPs:
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> findMin#(l)
minSort#(l) -> minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) -> minSort#(xs)
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_9) = {1},
uargs(c_13) = {1},
uargs(c_15) = {1},
uargs(c_16) = {1},
uargs(c_17) = {1},
uargs(c_18) = {1,2},
uargs(c_20) = {1}
Following symbols are considered usable:
{findMin,findMin#1,findMin#2,findMin#3,#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#,findMin#3#
,minSort#,minSort#1#}
TcT has computed the following interpretation:
p(#0) = [1]
[0]
p(#EQ) = [0]
[0]
p(#GT) = [2]
[0]
p(#LT) = [0]
[2]
p(#cklt) = [1]
[0]
p(#compare) = [1 3] x1 + [0 2] x2 + [0]
[2 0] [0 0] [0]
p(#false) = [0]
[0]
p(#less) = [2 0] x1 + [0 0] x2 + [0]
[1 2] [2 1] [0]
p(#neg) = [0 0] x1 + [1]
[0 1] [1]
p(#pos) = [0 2] x1 + [1]
[0 1] [1]
p(#s) = [0 2] x1 + [0]
[0 1] [0]
p(#true) = [0]
[0]
p(dd) = [0 0] x1 + [1 1] x2 + [0]
[0 1] [0 1] [0]
p(findMin) = [1 1] x1 + [0]
[0 1] [0]
p(findMin#1) = [1 1] x1 + [0]
[0 1] [0]
p(findMin#2) = [1 1] x1 + [0 1] x2 + [0]
[0 1] [0 1] [0]
p(findMin#3) = [0 1] x2 + [0 1] x3 + [1 2] x4 + [0]
[0 1] [0 1] [0 1] [0]
p(minSort) = [0 0] x1 + [0]
[0 1] [0]
p(minSort#1) = [1]
[2]
p(nil) = [0]
[0]
p(#cklt#) = [2 1] x1 + [0]
[2 2] [0]
p(#compare#) = [0 1] x1 + [0 1] x2 + [0]
[0 0] [0 1] [0]
p(#less#) = [0 1] x1 + [0 1] x2 + [0]
[2 2] [0 0] [0]
p(findMin#) = [1 2] x1 + [0]
[0 0] [0]
p(findMin#1#) = [1 2] x1 + [0]
[1 0] [2]
p(findMin#2#) = [0 1] x1 + [0 1] x2 + [0]
[0 0] [3 2] [0]
p(findMin#3#) = [2]
[2]
p(minSort#) = [1 2] x1 + [0]
[0 0] [0]
p(minSort#1#) = [1 1] x1 + [0]
[0 0] [0]
p(c_1) = [1]
[0]
p(c_2) = [0]
[0]
p(c_3) = [0]
[2]
p(c_4) = [1]
[0]
p(c_5) = [1]
[0]
p(c_6) = [1]
[0]
p(c_7) = [2]
[0]
p(c_8) = [1]
[0]
p(c_9) = [1 0] x1 + [1]
[0 0] [0]
p(c_10) = [0]
[0]
p(c_11) = [1]
[0]
p(c_12) = [0]
[1]
p(c_13) = [1 0] x1 + [1]
[0 0] [0]
p(c_14) = [2]
[1]
p(c_15) = [1 0] x1 + [0]
[0 0] [0]
p(c_16) = [1 0] x1 + [0]
[0 0] [0]
p(c_17) = [1 0] x1 + [0]
[0 0] [0]
p(c_18) = [1 0] x1 + [1 1] x2 + [0]
[0 0] [0 0] [1]
p(c_19) = [1]
[2]
p(c_20) = [1 0] x1 + [0]
[0 1] [0]
p(c_21) = [0]
[0]
p(c_22) = [0]
[1]
p(c_23) = [1]
[2]
p(c_24) = [0 1] x1 + [1]
[0 1] [2]
p(c_25) = [0]
[0]
p(c_26) = [2]
[0]
Following rules are strictly oriented:
#compare#(#neg(x),#neg(y)) = [0 1] x + [0 1] y + [2]
[0 0] [0 1] [1]
> [0 1] x + [0 1] y + [1]
[0 0] [0 0] [0]
= c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) = [0 1] x + [0 1] y + [2]
[0 0] [0 1] [1]
> [0 1] x + [0 1] y + [1]
[0 0] [0 0] [0]
= c_13(#compare#(x,y))
Following rules are (at-least) weakly oriented:
#compare#(#s(x),#s(y)) = [0 1] x + [0 1] y + [0]
[0 0] [0 1] [0]
>= [0 1] x + [0 1] y + [0]
[0 0] [0 0] [0]
= c_15(#compare#(x,y))
#less#(x,y) = [0 1] x + [0 1] y + [0]
[2 2] [0 0] [0]
>= [0 1] x + [0 1] y + [0]
[0 0] [0 0] [0]
= c_16(#compare#(x,y))
findMin#(l) = [1 2] l + [0]
[0 0] [0]
>= [1 2] l + [0]
[0 0] [0]
= c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) = [0 2] x + [1 3] xs + [0]
[0 0] [1 1] [2]
>= [0 1] x + [1 3] xs + [0]
[0 0] [0 0] [1]
= c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) = [0 1] x + [0 1] y + [0 1] ys + [0]
[3 2] [0 0] [0 0] [0]
>= [0 1] x + [0 1] y + [0]
[2 2] [0 0] [0]
= c_20(#less#(x,y))
minSort#(l) = [1 2] l + [0]
[0 0] [0]
>= [1 2] l + [0]
[0 0] [0]
= findMin#(l)
minSort#(l) = [1 2] l + [0]
[0 0] [0]
>= [1 2] l + [0]
[0 0] [0]
= minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) = [0 1] x + [1 2] xs + [0]
[0 0] [0 0] [0]
>= [1 2] xs + [0]
[0 0] [0]
= minSort#(xs)
findMin(l) = [1 1] l + [0]
[0 1] [0]
>= [1 1] l + [0]
[0 1] [0]
= findMin#1(l)
findMin#1(dd(x,xs)) = [0 1] x + [1 2] xs + [0]
[0 1] [0 1] [0]
>= [0 1] x + [1 2] xs + [0]
[0 1] [0 1] [0]
= findMin#2(findMin(xs),x)
findMin#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
findMin#2(dd(y,ys),x) = [0 1] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
>= [0 1] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
= findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) = [0 1] x + [0]
[0 1] [0]
>= [0 0] x + [0]
[0 1] [0]
= dd(x,nil())
findMin#3(#false(),x,y,ys) = [0 1] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
>= [0 1] x + [0 0] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
= dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) = [0 1] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
>= [0 0] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
= dd(x,dd(y,ys))
**** Step 6.a:1.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
- Weak DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> findMin#(l)
minSort#(l) -> minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) -> minSort#(xs)
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
**** Step 6.a:1.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
- Weak DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> findMin#(l)
minSort#(l) -> minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) -> minSort#(xs)
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ 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}}
+ Details:
We first use the processor NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
The strictly oriented rules are moved into the weak component.
***** Step 6.a:1.b:1.b:1.a:1: NaturalMI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
- Weak DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> findMin#(l)
minSort#(l) -> minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) -> minSort#(xs)
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
NaturalMI {miDimension = 2, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_9) = {1},
uargs(c_13) = {1},
uargs(c_15) = {1},
uargs(c_16) = {1},
uargs(c_17) = {1},
uargs(c_18) = {1,2},
uargs(c_20) = {1}
Following symbols are considered usable:
{findMin,findMin#1,findMin#2,findMin#3,#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#,findMin#3#
,minSort#,minSort#1#}
TcT has computed the following interpretation:
p(#0) = [0]
[0]
p(#EQ) = [0]
[1]
p(#GT) = [0]
[3]
p(#LT) = [0]
[1]
p(#cklt) = [0 0] x1 + [0]
[0 1] [3]
p(#compare) = [0 0] x1 + [0 0] x2 + [0]
[1 1] [0 1] [0]
p(#false) = [1]
[0]
p(#less) = [1 0] x1 + [2 2] x2 + [0]
[2 0] [0 0] [0]
p(#neg) = [0 0] x1 + [0]
[0 1] [0]
p(#pos) = [0 2] x1 + [0]
[0 1] [2]
p(#s) = [0 1] x1 + [3]
[0 1] [1]
p(#true) = [0]
[0]
p(dd) = [0 0] x1 + [1 1] x2 + [0]
[0 1] [0 1] [0]
p(findMin) = [1 1] x1 + [0]
[0 1] [0]
p(findMin#1) = [1 1] x1 + [0]
[0 1] [0]
p(findMin#2) = [1 1] x1 + [0 1] x2 + [0]
[0 1] [0 1] [0]
p(findMin#3) = [0 1] x2 + [0 1] x3 + [1 2] x4 + [0]
[0 1] [0 1] [0 1] [0]
p(minSort) = [0 0] x1 + [0]
[1 0] [0]
p(minSort#1) = [2]
[1]
p(nil) = [0]
[0]
p(#cklt#) = [0 1] x1 + [2]
[1 0] [2]
p(#compare#) = [0 1] x1 + [0 1] x2 + [0]
[0 2] [0 0] [1]
p(#less#) = [0 1] x1 + [0 1] x2 + [0]
[0 1] [0 0] [0]
p(findMin#) = [1 2] x1 + [0]
[0 0] [0]
p(findMin#1#) = [1 2] x1 + [0]
[2 3] [2]
p(findMin#2#) = [0 1] x1 + [0 2] x2 + [0]
[2 0] [0 2] [0]
p(findMin#3#) = [0 0] x1 + [1 0] x2 + [0 2] x4 + [0]
[0 2] [0 1] [2 0] [2]
p(minSort#) = [2 2] x1 + [0]
[0 0] [0]
p(minSort#1#) = [2 0] x1 + [0]
[0 0] [0]
p(c_1) = [2]
[0]
p(c_2) = [0]
[0]
p(c_3) = [0]
[0]
p(c_4) = [0]
[1]
p(c_5) = [1]
[0]
p(c_6) = [2]
[0]
p(c_7) = [0]
[1]
p(c_8) = [1]
[2]
p(c_9) = [1 0] x1 + [0]
[0 0] [0]
p(c_10) = [0]
[0]
p(c_11) = [1]
[1]
p(c_12) = [2]
[0]
p(c_13) = [1 0] x1 + [2]
[0 1] [1]
p(c_14) = [0]
[0]
p(c_15) = [1 0] x1 + [1]
[0 0] [1]
p(c_16) = [1 0] x1 + [0]
[0 0] [0]
p(c_17) = [1 0] x1 + [0]
[0 0] [0]
p(c_18) = [1 0] x1 + [1 0] x2 + [0]
[1 0] [2 0] [1]
p(c_19) = [0]
[0]
p(c_20) = [1 1] x1 + [0]
[0 0] [0]
p(c_21) = [1]
[1]
p(c_22) = [1]
[0]
p(c_23) = [0]
[1]
p(c_24) = [0 0] x2 + [0]
[0 1] [1]
p(c_25) = [1]
[0]
p(c_26) = [1]
[0]
Following rules are strictly oriented:
#compare#(#s(x),#s(y)) = [0 1] x + [0 1] y + [2]
[0 2] [0 0] [3]
> [0 1] x + [0 1] y + [1]
[0 0] [0 0] [1]
= c_15(#compare#(x,y))
Following rules are (at-least) weakly oriented:
#compare#(#neg(x),#neg(y)) = [0 1] x + [0 1] y + [0]
[0 2] [0 0] [1]
>= [0 1] x + [0 1] y + [0]
[0 0] [0 0] [0]
= c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) = [0 1] x + [0 1] y + [4]
[0 2] [0 0] [5]
>= [0 1] x + [0 1] y + [2]
[0 2] [0 0] [2]
= c_13(#compare#(x,y))
#less#(x,y) = [0 1] x + [0 1] y + [0]
[0 1] [0 0] [0]
>= [0 1] x + [0 1] y + [0]
[0 0] [0 0] [0]
= c_16(#compare#(x,y))
findMin#(l) = [1 2] l + [0]
[0 0] [0]
>= [1 2] l + [0]
[0 0] [0]
= c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) = [0 2] x + [1 3] xs + [0]
[0 3] [2 5] [2]
>= [0 2] x + [1 3] xs + [0]
[0 2] [2 5] [1]
= c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) = [0 2] x + [0 1] y + [0 1] ys + [0]
[0 2] [0 0] [2 2] [0]
>= [0 2] x + [0 1] y + [0]
[0 0] [0 0] [0]
= c_20(#less#(x,y))
minSort#(l) = [2 2] l + [0]
[0 0] [0]
>= [1 2] l + [0]
[0 0] [0]
= findMin#(l)
minSort#(l) = [2 2] l + [0]
[0 0] [0]
>= [2 2] l + [0]
[0 0] [0]
= minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) = [2 2] xs + [0]
[0 0] [0]
>= [2 2] xs + [0]
[0 0] [0]
= minSort#(xs)
findMin(l) = [1 1] l + [0]
[0 1] [0]
>= [1 1] l + [0]
[0 1] [0]
= findMin#1(l)
findMin#1(dd(x,xs)) = [0 1] x + [1 2] xs + [0]
[0 1] [0 1] [0]
>= [0 1] x + [1 2] xs + [0]
[0 1] [0 1] [0]
= findMin#2(findMin(xs),x)
findMin#1(nil()) = [0]
[0]
>= [0]
[0]
= nil()
findMin#2(dd(y,ys),x) = [0 1] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
>= [0 1] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
= findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) = [0 1] x + [0]
[0 1] [0]
>= [0 0] x + [0]
[0 1] [0]
= dd(x,nil())
findMin#3(#false(),x,y,ys) = [0 1] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
>= [0 1] x + [0 0] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
= dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) = [0 1] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
>= [0 0] x + [0 1] y + [1 2] ys + [0]
[0 1] [0 1] [0 1] [0]
= dd(x,dd(y,ys))
***** Step 6.a:1.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> findMin#(l)
minSort#(l) -> minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) -> minSort#(xs)
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 6.a:1.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> findMin#(l)
minSort#(l) -> minSort#1#(findMin(l))
minSort#1#(dd(x,xs)) -> minSort#(xs)
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
2:W:#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
3:W:#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
4:W:#less#(x,y) -> c_16(#compare#(x,y))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):3
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):2
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):1
5:W:findMin#(l) -> c_17(findMin#1#(l))
-->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)):6
6:W:findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
-->_1 findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)):7
-->_2 findMin#(l) -> c_17(findMin#1#(l)):5
7:W:findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
-->_1 #less#(x,y) -> c_16(#compare#(x,y)):4
8:W:minSort#(l) -> findMin#(l)
-->_1 findMin#(l) -> c_17(findMin#1#(l)):5
9:W:minSort#(l) -> minSort#1#(findMin(l))
-->_1 minSort#1#(dd(x,xs)) -> minSort#(xs):10
10:W:minSort#1#(dd(x,xs)) -> minSort#(xs)
-->_1 minSort#(l) -> minSort#1#(findMin(l)):9
-->_1 minSort#(l) -> findMin#(l):8
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: minSort#(l) -> minSort#1#(findMin(l))
10: minSort#1#(dd(x,xs)) -> minSort#(xs)
8: minSort#(l) -> findMin#(l)
5: findMin#(l) -> c_17(findMin#1#(l))
6: findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
7: findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
4: #less#(x,y) -> c_16(#compare#(x,y))
1: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
3: #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
2: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
***** Step 6.a:1.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
** Step 6.b:1: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
#less#(x,y) -> c_16(#compare#(x,y))
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{1}
by application of
Pre({1}) = {4}.
Here rules are labelled as follows:
1: #less#(x,y) -> c_16(#compare#(x,y))
2: findMin#(l) -> c_17(findMin#1#(l))
3: findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
4: findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
5: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
6: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
7: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
8: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
9: #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
** Step 6.b:2: PredecessorEstimation WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#compare#(x,y))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
PredecessorEstimation {onSelection = all simple predecessor estimation selector}
+ Details:
We estimate the number of application of
{3}
by application of
Pre({3}) = {2}.
Here rules are labelled as follows:
1: findMin#(l) -> c_17(findMin#1#(l))
2: findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
3: findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
4: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
5: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
6: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
7: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
8: #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
9: #less#(x,y) -> c_16(#compare#(x,y))
** Step 6.b:3: RemoveWeakSuffixes WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak DPs:
#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
#less#(x,y) -> c_16(#compare#(x,y))
findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:findMin#(l) -> c_17(findMin#1#(l))
-->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)):2
2:S:findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
-->_1 findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)):9
-->_2 findMin#(l) -> c_17(findMin#1#(l)):1
3:S:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
-->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):4
-->_2 findMin#(l) -> c_17(findMin#1#(l)):1
4:S:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
-->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):3
5:W:#compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):7
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):6
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):5
6:W:#compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):7
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):6
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):5
7:W:#compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):7
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):6
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):5
8:W:#less#(x,y) -> c_16(#compare#(x,y))
-->_1 #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)):7
-->_1 #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)):6
-->_1 #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)):5
9:W:findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
-->_1 #less#(x,y) -> c_16(#compare#(x,y)):8
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
9: findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y))
8: #less#(x,y) -> c_16(#compare#(x,y))
7: #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y))
6: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y))
5: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x))
** Step 6.b:4: SimplifyRHS WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/2,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:findMin#(l) -> c_17(findMin#1#(l))
-->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)):2
2:S:findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs))
-->_2 findMin#(l) -> c_17(findMin#1#(l)):1
3:S:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
-->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):4
-->_2 findMin#(l) -> c_17(findMin#1#(l)):1
4:S:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
-->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):3
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
** Step 6.b:5: Decompose WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd}
+ Details:
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 DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
- Weak DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0
,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0
,c_22/0,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
Problem (S)
- Strict DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0
,c_7/0,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0
,c_22/0,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
*** Step 6.b:5.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
- Weak DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
2: findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
The strictly oriented rules are moved into the weak component.
**** Step 6.b:5.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
- Weak DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_17) = {1},
uargs(c_18) = {1},
uargs(c_24) = {1,2},
uargs(c_25) = {1}
Following symbols are considered usable:
{findMin,findMin#1,findMin#2,findMin#3,#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#,findMin#3#
,minSort#,minSort#1#}
TcT has computed the following interpretation:
p(#0) = 2
p(#EQ) = 0
p(#GT) = 2
p(#LT) = 1
p(#cklt) = 0
p(#compare) = 2*x1
p(#false) = 0
p(#less) = x1^2
p(#neg) = 2
p(#pos) = 2 + x1
p(#s) = x1
p(#true) = 1
p(dd) = 1 + x2
p(findMin) = x1
p(findMin#1) = x1
p(findMin#2) = 1 + x1
p(findMin#3) = 2 + x4
p(minSort) = 0
p(minSort#1) = 0
p(nil) = 0
p(#cklt#) = 2*x1
p(#compare#) = 1 + 2*x1 + 2*x1*x2 + x2^2
p(#less#) = x2 + 2*x2^2
p(findMin#) = x1
p(findMin#1#) = x1
p(findMin#2#) = x1 + 2*x1*x2 + 2*x2
p(findMin#3#) = 1 + x1*x2 + 2*x1^2 + x2*x3 + 2*x2*x4 + x2^2 + x3*x4 + x3^2 + x4^2
p(minSort#) = 2 + 3*x1 + 2*x1^2
p(minSort#1#) = 2 + 2*x1 + 2*x1^2
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = 0
p(c_5) = 1
p(c_6) = 1
p(c_7) = 2
p(c_8) = 0
p(c_9) = 2 + x1
p(c_10) = 0
p(c_11) = 2
p(c_12) = 0
p(c_13) = 2 + x1
p(c_14) = 0
p(c_15) = x1
p(c_16) = 1
p(c_17) = x1
p(c_18) = x1
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
p(c_22) = 0
p(c_23) = 0
p(c_24) = x1 + x2
p(c_25) = x1
p(c_26) = 2
Following rules are strictly oriented:
findMin#1#(dd(x,xs)) = 1 + xs
> xs
= c_18(findMin#(xs))
Following rules are (at-least) weakly oriented:
findMin#(l) = l
>= l
= c_17(findMin#1#(l))
minSort#(l) = 2 + 3*l + 2*l^2
>= 2 + 3*l + 2*l^2
= c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) = 6 + 6*xs + 2*xs^2
>= 2 + 3*xs + 2*xs^2
= c_25(minSort#(xs))
findMin(l) = l
>= l
= findMin#1(l)
findMin#1(dd(x,xs)) = 1 + xs
>= 1 + xs
= findMin#2(findMin(xs),x)
findMin#1(nil()) = 0
>= 0
= nil()
findMin#2(dd(y,ys),x) = 2 + ys
>= 2 + ys
= findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) = 1
>= 1
= dd(x,nil())
findMin#3(#false(),x,y,ys) = 2 + ys
>= 2 + ys
= dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) = 2 + ys
>= 2 + ys
= dd(x,dd(y,ys))
**** Step 6.b:5.a:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
findMin#(l) -> c_17(findMin#1#(l))
- Weak DPs:
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
**** Step 6.b:5.a:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
findMin#(l) -> c_17(findMin#1#(l))
- Weak DPs:
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}}
+ Details:
We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
1: findMin#(l) -> c_17(findMin#1#(l))
Consider the set of all dependency pairs
1: findMin#(l) -> c_17(findMin#1#(l))
2: findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
3: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
4: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2))
SPACE(?,?)on application of the dependency pairs
{1}
These cover all (indirect) predecessors of dependency pairs
{1,2}
their number of applications is equally bounded.
The dependency pairs are shifted into the weak component.
***** Step 6.b:5.a:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict DPs:
findMin#(l) -> c_17(findMin#1#(l))
- Weak DPs:
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(c_17) = {1},
uargs(c_18) = {1},
uargs(c_24) = {1,2},
uargs(c_25) = {1}
Following symbols are considered usable:
{#cklt,#less,findMin,findMin#1,findMin#2,findMin#3,#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#}
TcT has computed the following interpretation:
p(#0) = 2
p(#EQ) = 0
p(#GT) = 0
p(#LT) = 0
p(#cklt) = 1
p(#compare) = 1 + x2
p(#false) = 1
p(#less) = 1
p(#neg) = 0
p(#pos) = 0
p(#s) = 1
p(#true) = 1
p(dd) = 2 + x1 + x2
p(findMin) = x1
p(findMin#1) = x1
p(findMin#2) = 2 + x1 + x2
p(findMin#3) = 2*x1 + x1*x2 + 2*x1^2 + x3 + x4
p(minSort) = 2 + x1
p(minSort#1) = 2 + 2*x1
p(nil) = 0
p(#cklt#) = 0
p(#compare#) = 2*x2 + x2^2
p(#less#) = 2 + 2*x2 + 2*x2^2
p(findMin#) = 2 + 2*x1
p(findMin#1#) = 2*x1
p(findMin#2#) = x1
p(findMin#3#) = x1*x4 + x2 + 2*x3 + 2*x4^2
p(minSort#) = 2 + 2*x1 + x1^2
p(minSort#1#) = x1^2
p(c_1) = 0
p(c_2) = 0
p(c_3) = 0
p(c_4) = 0
p(c_5) = 0
p(c_6) = 2
p(c_7) = 0
p(c_8) = 2
p(c_9) = 0
p(c_10) = 0
p(c_11) = 2
p(c_12) = 1
p(c_13) = x1
p(c_14) = 2
p(c_15) = 1
p(c_16) = 1
p(c_17) = 1 + x1
p(c_18) = x1
p(c_19) = 0
p(c_20) = 0
p(c_21) = 0
p(c_22) = 2
p(c_23) = 2
p(c_24) = x1 + x2
p(c_25) = x1
p(c_26) = 1
Following rules are strictly oriented:
findMin#(l) = 2 + 2*l
> 1 + 2*l
= c_17(findMin#1#(l))
Following rules are (at-least) weakly oriented:
findMin#1#(dd(x,xs)) = 4 + 2*x + 2*xs
>= 2 + 2*xs
= c_18(findMin#(xs))
minSort#(l) = 2 + 2*l + l^2
>= 2 + 2*l + l^2
= c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) = 4 + 4*x + 2*x*xs + x^2 + 4*xs + xs^2
>= 2 + 2*xs + xs^2
= c_25(minSort#(xs))
#cklt(#EQ()) = 1
>= 1
= #false()
#cklt(#GT()) = 1
>= 1
= #false()
#cklt(#LT()) = 1
>= 1
= #true()
#less(x,y) = 1
>= 1
= #cklt(#compare(x,y))
findMin(l) = l
>= l
= findMin#1(l)
findMin#1(dd(x,xs)) = 2 + x + xs
>= 2 + x + xs
= findMin#2(findMin(xs),x)
findMin#1(nil()) = 0
>= 0
= nil()
findMin#2(dd(y,ys),x) = 4 + x + y + ys
>= 4 + x + y + ys
= findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) = 2 + x
>= 2 + x
= dd(x,nil())
findMin#3(#false(),x,y,ys) = 4 + x + y + ys
>= 4 + x + y + ys
= dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) = 4 + x + y + ys
>= 4 + x + y + ys
= dd(x,dd(y,ys))
***** Step 6.b:5.a:1.b:1.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
***** Step 6.b:5.a:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:findMin#(l) -> c_17(findMin#1#(l))
-->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#(xs)):2
2:W:findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
-->_1 findMin#(l) -> c_17(findMin#1#(l)):1
3:W:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
-->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):4
-->_2 findMin#(l) -> c_17(findMin#1#(l)):1
4:W:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
-->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
4: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
1: findMin#(l) -> c_17(findMin#1#(l))
2: findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
***** Step 6.b:5.a:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
*** Step 6.b:5.b:1: RemoveWeakSuffixes WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak DPs:
findMin#(l) -> c_17(findMin#1#(l))
findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:S:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
-->_2 findMin#(l) -> c_17(findMin#1#(l)):3
-->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):2
2:S:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
-->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):1
3:W:findMin#(l) -> c_17(findMin#1#(l))
-->_1 findMin#1#(dd(x,xs)) -> c_18(findMin#(xs)):4
4:W:findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
-->_1 findMin#(l) -> c_17(findMin#1#(l)):3
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
3: findMin#(l) -> c_17(findMin#1#(l))
4: findMin#1#(dd(x,xs)) -> c_18(findMin#(xs))
*** Step 6.b:5.b:2: SimplifyRHS WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/2,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
SimplifyRHS
+ Details:
Consider the dependency graph
1:S:minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l))
-->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):2
2:S:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
-->_1 minSort#(l) -> c_24(minSort#1#(findMin(l)),findMin#(l)):1
Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified:
minSort#(l) -> c_24(minSort#1#(findMin(l)))
*** Step 6.b:5.b:3: PredecessorEstimationCP WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/1,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ 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}}
+ Details:
We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
2: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
Consider the set of all dependency pairs
1: minSort#(l) -> c_24(minSort#1#(findMin(l)))
2: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1))
SPACE(?,?)on application of the dependency pairs
{2}
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.
**** Step 6.b:5.b:3.a:1: NaturalMI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/1,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
+ Details:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(c_24) = {1},
uargs(c_25) = {1}
Following symbols are considered usable:
{findMin,findMin#1,findMin#2,findMin#3,#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#,findMin#3#
,minSort#,minSort#1#}
TcT has computed the following interpretation:
p(#0) = [9]
p(#EQ) = [1]
p(#GT) = [4]
p(#LT) = [4]
p(#cklt) = [5] x1 + [8]
p(#compare) = [2] x1 + [0]
p(#false) = [0]
p(#less) = [1] x1 + [1] x2 + [0]
p(#neg) = [1] x1 + [4]
p(#pos) = [1] x1 + [0]
p(#s) = [1] x1 + [0]
p(#true) = [0]
p(dd) = [1] x2 + [1]
p(findMin) = [1] x1 + [0]
p(findMin#1) = [1] x1 + [0]
p(findMin#2) = [1] x1 + [1]
p(findMin#3) = [1] x4 + [2]
p(minSort) = [1] x1 + [8]
p(minSort#1) = [8]
p(nil) = [0]
p(#cklt#) = [1] x1 + [2]
p(#compare#) = [2] x2 + [0]
p(#less#) = [2] x1 + [1] x2 + [1]
p(findMin#) = [1]
p(findMin#1#) = [1]
p(findMin#2#) = [1] x2 + [8]
p(findMin#3#) = [8] x2 + [4] x3 + [1] x4 + [1]
p(minSort#) = [4] x1 + [0]
p(minSort#1#) = [4] x1 + [0]
p(c_1) = [2]
p(c_2) = [1]
p(c_3) = [1]
p(c_4) = [1]
p(c_5) = [0]
p(c_6) = [1]
p(c_7) = [0]
p(c_8) = [0]
p(c_9) = [0]
p(c_10) = [0]
p(c_11) = [0]
p(c_12) = [0]
p(c_13) = [1] x1 + [1]
p(c_14) = [1]
p(c_15) = [1] x1 + [0]
p(c_16) = [2] x1 + [1]
p(c_17) = [4] x1 + [1]
p(c_18) = [0]
p(c_19) = [1]
p(c_20) = [1] x1 + [1]
p(c_21) = [0]
p(c_22) = [2]
p(c_23) = [2]
p(c_24) = [1] x1 + [0]
p(c_25) = [1] x1 + [0]
p(c_26) = [4]
Following rules are strictly oriented:
minSort#1#(dd(x,xs)) = [4] xs + [4]
> [4] xs + [0]
= c_25(minSort#(xs))
Following rules are (at-least) weakly oriented:
minSort#(l) = [4] l + [0]
>= [4] l + [0]
= c_24(minSort#1#(findMin(l)))
findMin(l) = [1] l + [0]
>= [1] l + [0]
= findMin#1(l)
findMin#1(dd(x,xs)) = [1] xs + [1]
>= [1] xs + [1]
= findMin#2(findMin(xs),x)
findMin#1(nil()) = [0]
>= [0]
= nil()
findMin#2(dd(y,ys),x) = [1] ys + [2]
>= [1] ys + [2]
= findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) = [1]
>= [1]
= dd(x,nil())
findMin#3(#false(),x,y,ys) = [1] ys + [2]
>= [1] ys + [2]
= dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) = [1] ys + [2]
>= [1] ys + [2]
= dd(x,dd(y,ys))
**** Step 6.b:5.b:3.a:2: Assumption WORST_CASE(?,O(1))
+ Considered Problem:
- Strict DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)))
- Weak DPs:
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/1,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}}
+ Details:
()
**** Step 6.b:5.b:3.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1))
+ Considered Problem:
- Weak DPs:
minSort#(l) -> c_24(minSort#1#(findMin(l)))
minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/1,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
RemoveWeakSuffixes
+ Details:
Consider the dependency graph
1:W:minSort#(l) -> c_24(minSort#1#(findMin(l)))
-->_1 minSort#1#(dd(x,xs)) -> c_25(minSort#(xs)):2
2:W:minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
-->_1 minSort#(l) -> c_24(minSort#1#(findMin(l))):1
The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
1: minSort#(l) -> c_24(minSort#1#(findMin(l)))
2: minSort#1#(dd(x,xs)) -> c_25(minSort#(xs))
**** Step 6.b:5.b:3.b:2: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
#cklt(#EQ()) -> #false()
#cklt(#GT()) -> #false()
#cklt(#LT()) -> #true()
#compare(#0(),#0()) -> #EQ()
#compare(#0(),#neg(y)) -> #GT()
#compare(#0(),#pos(y)) -> #LT()
#compare(#0(),#s(y)) -> #LT()
#compare(#neg(x),#0()) -> #LT()
#compare(#neg(x),#neg(y)) -> #compare(y,x)
#compare(#neg(x),#pos(y)) -> #LT()
#compare(#pos(x),#0()) -> #GT()
#compare(#pos(x),#neg(y)) -> #GT()
#compare(#pos(x),#pos(y)) -> #compare(x,y)
#compare(#s(x),#0()) -> #GT()
#compare(#s(x),#s(y)) -> #compare(x,y)
#less(x,y) -> #cklt(#compare(x,y))
findMin(l) -> findMin#1(l)
findMin#1(dd(x,xs)) -> findMin#2(findMin(xs),x)
findMin#1(nil()) -> nil()
findMin#2(dd(y,ys),x) -> findMin#3(#less(x,y),x,y,ys)
findMin#2(nil(),x) -> dd(x,nil())
findMin#3(#false(),x,y,ys) -> dd(y,dd(x,ys))
findMin#3(#true(),x,y,ys) -> dd(x,dd(y,ys))
- Signature:
{#cklt/1,#compare/2,#less/2,findMin/1,findMin#1/1,findMin#2/2,findMin#3/4,minSort/1,minSort#1/1,#cklt#/1
,#compare#/2,#less#/2,findMin#/1,findMin#1#/1,findMin#2#/2,findMin#3#/4,minSort#/1,minSort#1#/1} / {#0/0
,#EQ/0,#GT/0,#LT/0,#false/0,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/0,c_6/0,c_7/0
,c_8/0,c_9/1,c_10/0,c_11/0,c_12/0,c_13/1,c_14/0,c_15/1,c_16/1,c_17/1,c_18/1,c_19/0,c_20/1,c_21/0,c_22/0
,c_23/0,c_24/1,c_25/1,c_26/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#
,findMin#3#,minSort#,minSort#1#} and constructors {#0,#EQ,#GT,#LT,#false,#neg,#pos,#s,#true,dd,nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^3))