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: 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)) 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: 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 3: 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)) 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: 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 4: 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)) 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: 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 5: UsableRules 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)) 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/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: 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)) #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)) * Step 6: 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)) #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 = Nothing, 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: 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/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: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.a:2: WeightGap 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/2,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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(minSort#1#) = {1}, uargs(c_24) = {1}, uargs(c_25) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [0] p(#pos) = [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(dd) = [0] p(findMin) = [0] p(findMin#1) = [0] p(findMin#2) = [1] x1 + [0] p(findMin#3) = [1] x1 + [0] p(minSort) = [0] p(minSort#1) = [0] p(nil) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [0] p(findMin#) = [0] p(findMin#1#) = [0] p(findMin#2#) = [0] p(findMin#3#) = [0] p(minSort#) = [0] p(minSort#1#) = [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) = [0] 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) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [2] p(c_22) = [2] p(c_23) = [1] p(c_24) = [1] x1 + [0] p(c_25) = [1] x1 + [0] p(c_26) = [0] Following rules are strictly oriented: minSort#1#(dd(x,xs)) = [2] > [0] = c_25(minSort#(xs)) Following rules are (at-least) weakly oriented: minSort#(l) = [0] >= [2] = c_24(minSort#1#(findMin(l))) #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(y)) = [0] >= [0] = #GT() #compare(#0(),#pos(y)) = [0] >= [0] = #LT() #compare(#0(),#s(y)) = [0] >= [0] = #LT() #compare(#neg(x),#0()) = [0] >= [0] = #LT() #compare(#neg(x),#neg(y)) = [0] >= [0] = #compare(y,x) #compare(#neg(x),#pos(y)) = [0] >= [0] = #LT() #compare(#pos(x),#0()) = [0] >= [0] = #GT() #compare(#pos(x),#neg(y)) = [0] >= [0] = #GT() #compare(#pos(x),#pos(y)) = [0] >= [0] = #compare(x,y) #compare(#s(x),#0()) = [0] >= [0] = #GT() #compare(#s(x),#s(y)) = [0] >= [0] = #compare(x,y) #less(x,y) = [0] >= [0] = #cklt(#compare(x,y)) findMin(l) = [0] >= [0] = findMin#1(l) findMin#1(dd(x,xs)) = [0] >= [0] = findMin#2(findMin(xs),x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(dd(y,ys),x) = [0] >= [0] = findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) = [0] >= [0] = dd(x,nil()) findMin#3(#false(),x,y,ys) = [0] >= [0] = dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) = [0] >= [0] = dd(x,dd(y,ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:3: WeightGap WORST_CASE(?,O(n^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/2,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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(minSort#1#) = {1}, uargs(c_24) = {1}, uargs(c_25) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#cklt) = [1] x1 + [2] p(#compare) = [0] p(#false) = [2] p(#less) = [2] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [2] p(dd) = [1] x1 + [1] x2 + [1] p(findMin) = [1] x1 + [0] p(findMin#1) = [1] x1 + [0] p(findMin#2) = [1] x1 + [1] x2 + [1] p(findMin#3) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(minSort) = [0] p(minSort#1) = [0] p(nil) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [0] p(findMin#) = [0] p(findMin#1#) = [0] p(findMin#2#) = [0] p(findMin#3#) = [0] p(minSort#) = [1] x1 + [5] p(minSort#1#) = [1] x1 + [4] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] 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) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [4] p(c_23) = [2] p(c_24) = [1] x1 + [0] p(c_25) = [1] x1 + [0] p(c_26) = [0] Following rules are strictly oriented: minSort#(l) = [1] l + [5] > [1] l + [4] = c_24(minSort#1#(findMin(l))) Following rules are (at-least) weakly oriented: minSort#1#(dd(x,xs)) = [1] x + [1] xs + [5] >= [1] xs + [5] = c_25(minSort#(xs)) #cklt(#EQ()) = [2] >= [2] = #false() #cklt(#GT()) = [2] >= [2] = #false() #cklt(#LT()) = [2] >= [2] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(y)) = [0] >= [0] = #GT() #compare(#0(),#pos(y)) = [0] >= [0] = #LT() #compare(#0(),#s(y)) = [0] >= [0] = #LT() #compare(#neg(x),#0()) = [0] >= [0] = #LT() #compare(#neg(x),#neg(y)) = [0] >= [0] = #compare(y,x) #compare(#neg(x),#pos(y)) = [0] >= [0] = #LT() #compare(#pos(x),#0()) = [0] >= [0] = #GT() #compare(#pos(x),#neg(y)) = [0] >= [0] = #GT() #compare(#pos(x),#pos(y)) = [0] >= [0] = #compare(x,y) #compare(#s(x),#0()) = [0] >= [0] = #GT() #compare(#s(x),#s(y)) = [0] >= [0] = #compare(x,y) #less(x,y) = [2] >= [2] = #cklt(#compare(x,y)) findMin(l) = [1] l + [0] >= [1] l + [0] = findMin#1(l) findMin#1(dd(x,xs)) = [1] x + [1] xs + [1] >= [1] x + [1] xs + [1] = findMin#2(findMin(xs),x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(dd(y,ys),x) = [1] x + [1] y + [1] ys + [2] >= [1] x + [1] y + [1] ys + [2] = findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) = [1] x + [1] >= [1] x + [1] = dd(x,nil()) findMin#3(#false(),x,y,ys) = [1] x + [1] y + [1] ys + [2] >= [1] x + [1] y + [1] ys + [2] = dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) = [1] x + [1] y + [1] ys + [2] >= [1] x + [1] y + [1] ys + [2] = dd(x,dd(y,ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 6.a:4: EmptyProcessor 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/2,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). ** Step 6.b:1: DecomposeDG 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)) #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)) - Weak DPs: 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: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#2#(findMin(xs),x),findMin#(xs)) minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> 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#2#(dd(y,ys),x) -> c_20(#less#(x,y)) Further, following extension rules are added to the lower component. findMin#(l) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) minSort#(l) -> findMin#(l) minSort#(l) -> minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) -> minSort#(xs) *** Step 6.b:1.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + 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)) - Weak DPs: 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: 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:W:minSort#(l) -> findMin#(l) -->_1 findMin#(l) -> c_17(findMin#1#(l)):1 4:W:minSort#(l) -> minSort#1#(findMin(l)) -->_1 minSort#1#(dd(x,xs)) -> minSort#(xs):5 5:W:minSort#1#(dd(x,xs)) -> minSort#(xs) -->_1 minSort#(l) -> minSort#1#(findMin(l)):4 -->_1 minSort#(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:1.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: findMin#(l) -> c_17(findMin#1#(l)) findMin#1#(dd(x,xs)) -> c_18(findMin#(xs)) - Weak DPs: 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/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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(minSort#1#) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(dd) = [0] p(findMin) = [0] p(findMin#1) = [0] p(findMin#2) = [1] x1 + [0] p(findMin#3) = [1] x1 + [0] p(minSort) = [0] p(minSort#1) = [0] p(nil) = [0] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [0] p(findMin#) = [0] p(findMin#1#) = [6] p(findMin#2#) = [0] p(findMin#3#) = [0] p(minSort#) = [0] p(minSort#1#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] 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) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] Following rules are strictly oriented: findMin#1#(dd(x,xs)) = [6] > [0] = c_18(findMin#(xs)) Following rules are (at-least) weakly oriented: findMin#(l) = [0] >= [6] = c_17(findMin#1#(l)) minSort#(l) = [0] >= [0] = findMin#(l) minSort#(l) = [0] >= [0] = minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) = [0] >= [0] = minSort#(xs) #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(y)) = [0] >= [0] = #GT() #compare(#0(),#pos(y)) = [0] >= [0] = #LT() #compare(#0(),#s(y)) = [0] >= [0] = #LT() #compare(#neg(x),#0()) = [0] >= [0] = #LT() #compare(#neg(x),#neg(y)) = [0] >= [0] = #compare(y,x) #compare(#neg(x),#pos(y)) = [0] >= [0] = #LT() #compare(#pos(x),#0()) = [0] >= [0] = #GT() #compare(#pos(x),#neg(y)) = [0] >= [0] = #GT() #compare(#pos(x),#pos(y)) = [0] >= [0] = #compare(x,y) #compare(#s(x),#0()) = [0] >= [0] = #GT() #compare(#s(x),#s(y)) = [0] >= [0] = #compare(x,y) #less(x,y) = [0] >= [0] = #cklt(#compare(x,y)) findMin(l) = [0] >= [0] = findMin#1(l) findMin#1(dd(x,xs)) = [0] >= [0] = findMin#2(findMin(xs),x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(dd(y,ys),x) = [0] >= [0] = findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) = [0] >= [0] = dd(x,nil()) findMin#3(#false(),x,y,ys) = [0] >= [0] = dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) = [0] >= [0] = dd(x,dd(y,ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:3: WeightGap WORST_CASE(?,O(n^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) -> 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/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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(minSort#1#) = {1}, uargs(c_17) = {1}, uargs(c_18) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [2] p(#GT) = [2] p(#LT) = [2] p(#cklt) = [1] x1 + [0] p(#compare) = [2] p(#false) = [2] p(#less) = [2] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [2] 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] x1 + [1] x4 + [0] p(minSort) = [0] p(minSort#1) = [2] p(nil) = [1] p(#cklt#) = [0] p(#compare#) = [0] p(#less#) = [1] x2 + [0] p(findMin#) = [1] x1 + [3] p(findMin#1#) = [1] x1 + [2] p(findMin#2#) = [1] x1 + [1] x2 + [1] p(findMin#3#) = [2] x1 + [1] x2 + [1] x4 + [0] p(minSort#) = [1] x1 + [3] p(minSort#1#) = [1] x1 + [3] p(c_1) = [1] p(c_2) = [0] p(c_3) = [4] p(c_4) = [2] p(c_5) = [0] p(c_6) = [4] p(c_7) = [1] p(c_8) = [0] p(c_9) = [0] p(c_10) = [4] p(c_11) = [0] p(c_12) = [2] p(c_13) = [1] p(c_14) = [0] p(c_15) = [1] x1 + [1] p(c_16) = [1] x1 + [0] p(c_17) = [1] x1 + [0] p(c_18) = [1] x1 + [0] p(c_19) = [2] p(c_20) = [1] x1 + [1] p(c_21) = [1] p(c_22) = [2] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] Following rules are strictly oriented: findMin#(l) = [1] l + [3] > [1] l + [2] = c_17(findMin#1#(l)) Following rules are (at-least) weakly oriented: findMin#1#(dd(x,xs)) = [1] xs + [3] >= [1] xs + [3] = c_18(findMin#(xs)) minSort#(l) = [1] l + [3] >= [1] l + [3] = findMin#(l) minSort#(l) = [1] l + [3] >= [1] l + [3] = minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) = [1] xs + [4] >= [1] xs + [3] = minSort#(xs) #cklt(#EQ()) = [2] >= [2] = #false() #cklt(#GT()) = [2] >= [2] = #false() #cklt(#LT()) = [2] >= [2] = #true() #compare(#0(),#0()) = [2] >= [2] = #EQ() #compare(#0(),#neg(y)) = [2] >= [2] = #GT() #compare(#0(),#pos(y)) = [2] >= [2] = #LT() #compare(#0(),#s(y)) = [2] >= [2] = #LT() #compare(#neg(x),#0()) = [2] >= [2] = #LT() #compare(#neg(x),#neg(y)) = [2] >= [2] = #compare(y,x) #compare(#neg(x),#pos(y)) = [2] >= [2] = #LT() #compare(#pos(x),#0()) = [2] >= [2] = #GT() #compare(#pos(x),#neg(y)) = [2] >= [2] = #GT() #compare(#pos(x),#pos(y)) = [2] >= [2] = #compare(x,y) #compare(#s(x),#0()) = [2] >= [2] = #GT() #compare(#s(x),#s(y)) = [2] >= [2] = #compare(x,y) #less(x,y) = [2] >= [2] = #cklt(#compare(x,y)) 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()) = [1] >= [1] = 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) = [2] >= [2] = 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)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.a:4: EmptyProcessor 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) -> 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/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:1.b:1: WeightGap WORST_CASE(?,O(n^1)) + 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#2#(dd(y,ys),x) -> c_20(#less#(x,y)) - Weak DPs: findMin#(l) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(findMin#2#) = {1}, uargs(minSort#1#) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1}, uargs(c_20) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(dd) = [0] p(findMin) = [0] p(findMin#1) = [0] p(findMin#2) = [1] x1 + [0] p(findMin#3) = [1] x1 + [0] p(minSort) = [0] p(minSort#1) = [0] p(nil) = [0] p(#cklt#) = [0] p(#compare#) = [4] p(#less#) = [7] p(findMin#) = [0] p(findMin#1#) = [0] p(findMin#2#) = [1] x1 + [0] p(findMin#3#) = [0] p(minSort#) = [0] p(minSort#1#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [2] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [4] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] Following rules are strictly oriented: #less#(x,y) = [7] > [6] = c_16(#compare#(x,y)) Following rules are (at-least) weakly oriented: #compare#(#neg(x),#neg(y)) = [4] >= [4] = c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) = [4] >= [4] = c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) = [4] >= [4] = c_15(#compare#(x,y)) findMin#(l) = [0] >= [0] = findMin#1#(l) findMin#1#(dd(x,xs)) = [0] >= [0] = findMin#(xs) findMin#1#(dd(x,xs)) = [0] >= [0] = findMin#2#(findMin(xs),x) findMin#2#(dd(y,ys),x) = [0] >= [11] = c_20(#less#(x,y)) minSort#(l) = [0] >= [0] = findMin#(l) minSort#(l) = [0] >= [0] = minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) = [0] >= [0] = minSort#(xs) #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(y)) = [0] >= [0] = #GT() #compare(#0(),#pos(y)) = [0] >= [0] = #LT() #compare(#0(),#s(y)) = [0] >= [0] = #LT() #compare(#neg(x),#0()) = [0] >= [0] = #LT() #compare(#neg(x),#neg(y)) = [0] >= [0] = #compare(y,x) #compare(#neg(x),#pos(y)) = [0] >= [0] = #LT() #compare(#pos(x),#0()) = [0] >= [0] = #GT() #compare(#pos(x),#neg(y)) = [0] >= [0] = #GT() #compare(#pos(x),#pos(y)) = [0] >= [0] = #compare(x,y) #compare(#s(x),#0()) = [0] >= [0] = #GT() #compare(#s(x),#s(y)) = [0] >= [0] = #compare(x,y) #less(x,y) = [0] >= [0] = #cklt(#compare(x,y)) findMin(l) = [0] >= [0] = findMin#1(l) findMin#1(dd(x,xs)) = [0] >= [0] = findMin#2(findMin(xs),x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(dd(y,ys),x) = [0] >= [0] = findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) = [0] >= [0] = dd(x,nil()) findMin#3(#false(),x,y,ys) = [0] >= [0] = dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) = [0] >= [0] = dd(x,dd(y,ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:2: WeightGap WORST_CASE(?,O(n^1)) + 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)) findMin#2#(dd(y,ys),x) -> c_20(#less#(x,y)) - Weak DPs: #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(findMin#2#) = {1}, uargs(minSort#1#) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1}, uargs(c_20) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [0] p(#true) = [0] p(dd) = [1] x2 + [0] p(findMin) = [0] p(findMin#1) = [0] p(findMin#2) = [1] x1 + [0] p(findMin#3) = [1] x1 + [1] x4 + [0] p(minSort) = [0] p(minSort#1) = [0] p(nil) = [0] p(#cklt#) = [0] p(#compare#) = [1] p(#less#) = [2] p(findMin#) = [3] p(findMin#1#) = [3] p(findMin#2#) = [1] x1 + [3] p(findMin#3#) = [0] p(minSort#) = [5] p(minSort#1#) = [1] x1 + [5] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [0] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [0] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [7] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [1] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] Following rules are strictly oriented: findMin#2#(dd(y,ys),x) = [1] ys + [3] > [2] = c_20(#less#(x,y)) Following rules are (at-least) weakly oriented: #compare#(#neg(x),#neg(y)) = [1] >= [1] = c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) = [1] >= [8] = c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) = [1] >= [1] = c_15(#compare#(x,y)) #less#(x,y) = [2] >= [2] = c_16(#compare#(x,y)) findMin#(l) = [3] >= [3] = findMin#1#(l) findMin#1#(dd(x,xs)) = [3] >= [3] = findMin#(xs) findMin#1#(dd(x,xs)) = [3] >= [3] = findMin#2#(findMin(xs),x) minSort#(l) = [5] >= [3] = findMin#(l) minSort#(l) = [5] >= [5] = minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) = [1] xs + [5] >= [5] = minSort#(xs) #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(y)) = [0] >= [0] = #GT() #compare(#0(),#pos(y)) = [0] >= [0] = #LT() #compare(#0(),#s(y)) = [0] >= [0] = #LT() #compare(#neg(x),#0()) = [0] >= [0] = #LT() #compare(#neg(x),#neg(y)) = [0] >= [0] = #compare(y,x) #compare(#neg(x),#pos(y)) = [0] >= [0] = #LT() #compare(#pos(x),#0()) = [0] >= [0] = #GT() #compare(#pos(x),#neg(y)) = [0] >= [0] = #GT() #compare(#pos(x),#pos(y)) = [0] >= [0] = #compare(x,y) #compare(#s(x),#0()) = [0] >= [0] = #GT() #compare(#s(x),#s(y)) = [0] >= [0] = #compare(x,y) #less(x,y) = [0] >= [0] = #cklt(#compare(x,y)) findMin(l) = [0] >= [0] = findMin#1(l) findMin#1(dd(x,xs)) = [0] >= [0] = findMin#2(findMin(xs),x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(dd(y,ys),x) = [1] ys + [0] >= [1] ys + [0] = findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) = [0] >= [0] = dd(x,nil()) findMin#3(#false(),x,y,ys) = [1] ys + [0] >= [1] ys + [0] = dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) = [1] ys + [0] >= [1] ys + [0] = dd(x,dd(y,ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:3: WeightGap WORST_CASE(?,O(n^1)) + 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) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(findMin#2#) = {1}, uargs(minSort#1#) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1}, uargs(c_20) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [4] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [0] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [1] p(#true) = [0] p(dd) = [1] x1 + [1] x2 + [0] p(findMin) = [1] x1 + [0] p(findMin#1) = [1] x1 + [0] p(findMin#2) = [1] x1 + [1] x2 + [0] p(findMin#3) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(minSort) = [1] p(minSort#1) = [1] p(nil) = [0] p(#cklt#) = [0] p(#compare#) = [1] x1 + [1] x2 + [0] p(#less#) = [1] x1 + [1] x2 + [0] p(findMin#) = [1] x1 + [0] p(findMin#1#) = [1] x1 + [0] p(findMin#2#) = [1] x1 + [1] x2 + [0] p(findMin#3#) = [2] x2 + [1] x3 + [1] x4 + [0] p(minSort#) = [1] x1 + [0] p(minSort#1#) = [1] x1 + [0] p(c_1) = [1] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [1] p(c_7) = [2] p(c_8) = [4] p(c_9) = [1] x1 + [0] p(c_10) = [2] p(c_11) = [0] p(c_12) = [0] p(c_13) = [1] x1 + [1] p(c_14) = [0] p(c_15) = [1] x1 + [1] p(c_16) = [1] x1 + [0] p(c_17) = [4] x1 + [1] p(c_18) = [1] x2 + [1] p(c_19) = [0] p(c_20) = [1] x1 + [0] p(c_21) = [1] p(c_22) = [1] p(c_23) = [1] p(c_24) = [1] p(c_25) = [0] p(c_26) = [1] Following rules are strictly oriented: #compare#(#s(x),#s(y)) = [1] x + [1] y + [2] > [1] x + [1] y + [1] = c_15(#compare#(x,y)) Following rules are (at-least) weakly oriented: #compare#(#neg(x),#neg(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [1] = c_13(#compare#(x,y)) #less#(x,y) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = c_16(#compare#(x,y)) findMin#(l) = [1] l + [0] >= [1] l + [0] = findMin#1#(l) findMin#1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] xs + [0] = findMin#(xs) findMin#1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = findMin#2#(findMin(xs),x) findMin#2#(dd(y,ys),x) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [0] = c_20(#less#(x,y)) minSort#(l) = [1] l + [0] >= [1] l + [0] = findMin#(l) minSort#(l) = [1] l + [0] >= [1] l + [0] = minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] xs + [0] = minSort#(xs) #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(y)) = [0] >= [0] = #GT() #compare(#0(),#pos(y)) = [0] >= [0] = #LT() #compare(#0(),#s(y)) = [0] >= [0] = #LT() #compare(#neg(x),#0()) = [0] >= [0] = #LT() #compare(#neg(x),#neg(y)) = [0] >= [0] = #compare(y,x) #compare(#neg(x),#pos(y)) = [0] >= [0] = #LT() #compare(#pos(x),#0()) = [0] >= [0] = #GT() #compare(#pos(x),#neg(y)) = [0] >= [0] = #GT() #compare(#pos(x),#pos(y)) = [0] >= [0] = #compare(x,y) #compare(#s(x),#0()) = [0] >= [0] = #GT() #compare(#s(x),#s(y)) = [0] >= [0] = #compare(x,y) #less(x,y) = [0] >= [0] = #cklt(#compare(x,y)) findMin(l) = [1] l + [0] >= [1] l + [0] = findMin#1(l) findMin#1(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = findMin#2(findMin(xs),x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(dd(y,ys),x) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) = [1] x + [0] >= [1] x + [0] = dd(x,nil()) findMin#3(#false(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(x,dd(y,ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:4: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) - Weak DPs: #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(findMin#2#) = {1}, uargs(minSort#1#) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1}, uargs(c_20) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [4] p(#pos) = [1] x1 + [0] p(#s) = [1] x1 + [1] p(#true) = [0] p(dd) = [1] x1 + [1] x2 + [0] p(findMin) = [1] x1 + [0] p(findMin#1) = [1] x1 + [0] p(findMin#2) = [1] x1 + [1] x2 + [0] p(findMin#3) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(minSort) = [0] p(minSort#1) = [0] p(nil) = [2] p(#cklt#) = [2] p(#compare#) = [1] x1 + [1] x2 + [0] p(#less#) = [1] x1 + [1] x2 + [0] p(findMin#) = [1] x1 + [0] p(findMin#1#) = [1] x1 + [0] p(findMin#2#) = [1] x1 + [1] x2 + [0] p(findMin#3#) = [0] p(minSort#) = [1] x1 + [1] p(minSort#1#) = [1] x1 + [1] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [4] p(c_8) = [0] p(c_9) = [1] x1 + [0] p(c_10) = [1] p(c_11) = [1] p(c_12) = [1] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [1] x1 + [0] p(c_16) = [1] x1 + [0] p(c_17) = [1] x1 + [4] p(c_18) = [4] x1 + [2] p(c_19) = [1] p(c_20) = [1] x1 + [0] p(c_21) = [1] p(c_22) = [0] p(c_23) = [0] p(c_24) = [1] x1 + [1] x2 + [0] p(c_25) = [1] x1 + [0] p(c_26) = [4] Following rules are strictly oriented: #compare#(#neg(x),#neg(y)) = [1] x + [1] y + [8] > [1] x + [1] y + [0] = c_9(#compare#(y,x)) Following rules are (at-least) weakly oriented: #compare#(#pos(x),#pos(y)) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = c_13(#compare#(x,y)) #compare#(#s(x),#s(y)) = [1] x + [1] y + [2] >= [1] x + [1] y + [0] = c_15(#compare#(x,y)) #less#(x,y) = [1] x + [1] y + [0] >= [1] x + [1] y + [0] = c_16(#compare#(x,y)) findMin#(l) = [1] l + [0] >= [1] l + [0] = findMin#1#(l) findMin#1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] xs + [0] = findMin#(xs) findMin#1#(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = findMin#2#(findMin(xs),x) findMin#2#(dd(y,ys),x) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [0] = c_20(#less#(x,y)) minSort#(l) = [1] l + [1] >= [1] l + [0] = findMin#(l) minSort#(l) = [1] l + [1] >= [1] l + [1] = minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) = [1] x + [1] xs + [1] >= [1] xs + [1] = minSort#(xs) #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(y)) = [0] >= [0] = #GT() #compare(#0(),#pos(y)) = [0] >= [0] = #LT() #compare(#0(),#s(y)) = [0] >= [0] = #LT() #compare(#neg(x),#0()) = [0] >= [0] = #LT() #compare(#neg(x),#neg(y)) = [0] >= [0] = #compare(y,x) #compare(#neg(x),#pos(y)) = [0] >= [0] = #LT() #compare(#pos(x),#0()) = [0] >= [0] = #GT() #compare(#pos(x),#neg(y)) = [0] >= [0] = #GT() #compare(#pos(x),#pos(y)) = [0] >= [0] = #compare(x,y) #compare(#s(x),#0()) = [0] >= [0] = #GT() #compare(#s(x),#s(y)) = [0] >= [0] = #compare(x,y) #less(x,y) = [0] >= [0] = #cklt(#compare(x,y)) findMin(l) = [1] l + [0] >= [1] l + [0] = findMin#1(l) findMin#1(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = findMin#2(findMin(xs),x) findMin#1(nil()) = [2] >= [2] = nil() findMin#2(dd(y,ys),x) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) = [1] x + [2] >= [1] x + [2] = dd(x,nil()) findMin#3(#false(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(x,dd(y,ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:5: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: #compare#(#pos(x),#pos(y)) -> c_13(#compare#(x,y)) - Weak DPs: #compare#(#neg(x),#neg(y)) -> c_9(#compare#(y,x)) #compare#(#s(x),#s(y)) -> c_15(#compare#(x,y)) #less#(x,y) -> c_16(#compare#(x,y)) findMin#(l) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) 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: WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(#cklt) = {1}, uargs(findMin#2) = {1}, uargs(findMin#3) = {1}, uargs(findMin#2#) = {1}, uargs(minSort#1#) = {1}, uargs(c_9) = {1}, uargs(c_13) = {1}, uargs(c_15) = {1}, uargs(c_16) = {1}, uargs(c_20) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [0] p(#GT) = [0] p(#LT) = [0] p(#cklt) = [1] x1 + [0] p(#compare) = [0] p(#false) = [0] p(#less) = [0] p(#neg) = [1] x1 + [1] p(#pos) = [1] x1 + [1] p(#s) = [1] x1 + [4] p(#true) = [0] p(dd) = [1] x1 + [1] x2 + [0] p(findMin) = [1] x1 + [0] p(findMin#1) = [1] x1 + [0] p(findMin#2) = [1] x1 + [1] x2 + [0] p(findMin#3) = [1] x1 + [1] x2 + [1] x3 + [1] x4 + [0] p(minSort) = [2] p(minSort#1) = [1] p(nil) = [0] p(#cklt#) = [4] p(#compare#) = [1] x1 + [1] x2 + [0] p(#less#) = [1] x1 + [1] x2 + [1] p(findMin#) = [1] x1 + [2] p(findMin#1#) = [1] x1 + [2] p(findMin#2#) = [1] x1 + [1] x2 + [2] p(findMin#3#) = [1] x2 + [1] x3 + [4] x4 + [1] p(minSort#) = [1] x1 + [4] p(minSort#1#) = [1] x1 + [4] p(c_1) = [1] p(c_2) = [0] p(c_3) = [0] p(c_4) = [4] p(c_5) = [2] p(c_6) = [1] p(c_7) = [1] p(c_8) = [2] p(c_9) = [1] x1 + [2] p(c_10) = [0] p(c_11) = [0] p(c_12) = [2] p(c_13) = [1] x1 + [1] p(c_14) = [1] p(c_15) = [1] x1 + [1] p(c_16) = [1] x1 + [0] p(c_17) = [0] p(c_18) = [1] x1 + [0] p(c_19) = [2] p(c_20) = [1] x1 + [0] p(c_21) = [2] p(c_22) = [0] p(c_23) = [1] p(c_24) = [4] x1 + [4] x2 + [0] p(c_25) = [1] x1 + [2] p(c_26) = [1] Following rules are strictly oriented: #compare#(#pos(x),#pos(y)) = [1] x + [1] y + [2] > [1] x + [1] y + [1] = c_13(#compare#(x,y)) Following rules are (at-least) weakly oriented: #compare#(#neg(x),#neg(y)) = [1] x + [1] y + [2] >= [1] x + [1] y + [2] = c_9(#compare#(y,x)) #compare#(#s(x),#s(y)) = [1] x + [1] y + [8] >= [1] x + [1] y + [1] = c_15(#compare#(x,y)) #less#(x,y) = [1] x + [1] y + [1] >= [1] x + [1] y + [0] = c_16(#compare#(x,y)) findMin#(l) = [1] l + [2] >= [1] l + [2] = findMin#1#(l) findMin#1#(dd(x,xs)) = [1] x + [1] xs + [2] >= [1] xs + [2] = findMin#(xs) findMin#1#(dd(x,xs)) = [1] x + [1] xs + [2] >= [1] x + [1] xs + [2] = findMin#2#(findMin(xs),x) findMin#2#(dd(y,ys),x) = [1] x + [1] y + [1] ys + [2] >= [1] x + [1] y + [1] = c_20(#less#(x,y)) minSort#(l) = [1] l + [4] >= [1] l + [2] = findMin#(l) minSort#(l) = [1] l + [4] >= [1] l + [4] = minSort#1#(findMin(l)) minSort#1#(dd(x,xs)) = [1] x + [1] xs + [4] >= [1] xs + [4] = minSort#(xs) #cklt(#EQ()) = [0] >= [0] = #false() #cklt(#GT()) = [0] >= [0] = #false() #cklt(#LT()) = [0] >= [0] = #true() #compare(#0(),#0()) = [0] >= [0] = #EQ() #compare(#0(),#neg(y)) = [0] >= [0] = #GT() #compare(#0(),#pos(y)) = [0] >= [0] = #LT() #compare(#0(),#s(y)) = [0] >= [0] = #LT() #compare(#neg(x),#0()) = [0] >= [0] = #LT() #compare(#neg(x),#neg(y)) = [0] >= [0] = #compare(y,x) #compare(#neg(x),#pos(y)) = [0] >= [0] = #LT() #compare(#pos(x),#0()) = [0] >= [0] = #GT() #compare(#pos(x),#neg(y)) = [0] >= [0] = #GT() #compare(#pos(x),#pos(y)) = [0] >= [0] = #compare(x,y) #compare(#s(x),#0()) = [0] >= [0] = #GT() #compare(#s(x),#s(y)) = [0] >= [0] = #compare(x,y) #less(x,y) = [0] >= [0] = #cklt(#compare(x,y)) findMin(l) = [1] l + [0] >= [1] l + [0] = findMin#1(l) findMin#1(dd(x,xs)) = [1] x + [1] xs + [0] >= [1] x + [1] xs + [0] = findMin#2(findMin(xs),x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(dd(y,ys),x) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = findMin#3(#less(x,y),x,y,ys) findMin#2(nil(),x) = [1] x + [0] >= [1] x + [0] = dd(x,nil()) findMin#3(#false(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(y,dd(x,ys)) findMin#3(#true(),x,y,ys) = [1] x + [1] y + [1] ys + [0] >= [1] x + [1] y + [1] ys + [0] = dd(x,dd(y,ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. *** Step 6.b:1.b:6: EmptyProcessor 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) -> findMin#1#(l) findMin#1#(dd(x,xs)) -> findMin#(xs) findMin#1#(dd(x,xs)) -> findMin#2#(findMin(xs),x) 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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))