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))