WORST_CASE(?,O(n^2)) * Step 1: DependencyPairs WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin(@l) -> findMin#1(@l) findMin#1(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort(@l) -> minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) -> ::(@x,minSort(@xs)) minSort#1(nil()) -> nil() - 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) - 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,::/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,::,nil} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs #less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)) findMin#1#(nil()) -> c_4() findMin#2#(::(@y,@ys),@x) -> c_5(findMin#3#(#less(@x,@y),@x,@y,@ys),#less#(@x,@y)) findMin#2#(nil(),@x) -> c_6() findMin#3#(#false(),@x,@y,@ys) -> c_7() findMin#3#(#true(),@x,@y,@ys) -> c_8() minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) minSort#1#(nil()) -> c_11() Weak DPs #cklt#(#EQ()) -> c_12() #cklt#(#GT()) -> c_13() #cklt#(#LT()) -> c_14() #compare#(#0(),#0()) -> c_15() #compare#(#0(),#neg(@y)) -> c_16() #compare#(#0(),#pos(@y)) -> c_17() #compare#(#0(),#s(@y)) -> c_18() #compare#(#neg(@x),#0()) -> c_19() #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_21() #compare#(#pos(@x),#0()) -> c_22() #compare#(#pos(@x),#neg(@y)) -> c_23() #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_25() #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)) and mark the set of starting terms. * Step 2: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: #less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)) findMin#1#(nil()) -> c_4() findMin#2#(::(@y,@ys),@x) -> c_5(findMin#3#(#less(@x,@y),@x,@y,@ys),#less#(@x,@y)) findMin#2#(nil(),@x) -> c_6() findMin#3#(#false(),@x,@y,@ys) -> c_7() findMin#3#(#true(),@x,@y,@ys) -> c_8() minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) minSort#1#(nil()) -> c_11() - Weak DPs: #cklt#(#EQ()) -> c_12() #cklt#(#GT()) -> c_13() #cklt#(#LT()) -> c_14() #compare#(#0(),#0()) -> c_15() #compare#(#0(),#neg(@y)) -> c_16() #compare#(#0(),#pos(@y)) -> c_17() #compare#(#0(),#s(@y)) -> c_18() #compare#(#neg(@x),#0()) -> c_19() #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_21() #compare#(#pos(@x),#0()) -> c_22() #compare#(#pos(@x),#neg(@y)) -> c_23() #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_25() #compare#(#s(@x),#s(@y)) -> c_26(#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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort(@l) -> minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) -> ::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,nil} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,4,6,7,8,11} by application of Pre({1,4,6,7,8,11}) = {2,3,5,9}. Here rules are labelled as follows: 1: #less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) 2: findMin#(@l) -> c_2(findMin#1#(@l)) 3: findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)) 4: findMin#1#(nil()) -> c_4() 5: findMin#2#(::(@y,@ys),@x) -> c_5(findMin#3#(#less(@x,@y),@x,@y,@ys),#less#(@x,@y)) 6: findMin#2#(nil(),@x) -> c_6() 7: findMin#3#(#false(),@x,@y,@ys) -> c_7() 8: findMin#3#(#true(),@x,@y,@ys) -> c_8() 9: minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) 10: minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) 11: minSort#1#(nil()) -> c_11() 12: #cklt#(#EQ()) -> c_12() 13: #cklt#(#GT()) -> c_13() 14: #cklt#(#LT()) -> c_14() 15: #compare#(#0(),#0()) -> c_15() 16: #compare#(#0(),#neg(@y)) -> c_16() 17: #compare#(#0(),#pos(@y)) -> c_17() 18: #compare#(#0(),#s(@y)) -> c_18() 19: #compare#(#neg(@x),#0()) -> c_19() 20: #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)) 21: #compare#(#neg(@x),#pos(@y)) -> c_21() 22: #compare#(#pos(@x),#0()) -> c_22() 23: #compare#(#pos(@x),#neg(@y)) -> c_23() 24: #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)) 25: #compare#(#s(@x),#0()) -> c_25() 26: #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)) * Step 3: PredecessorEstimation WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)) findMin#2#(::(@y,@ys),@x) -> c_5(findMin#3#(#less(@x,@y),@x,@y,@ys),#less#(@x,@y)) minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) - Weak DPs: #cklt#(#EQ()) -> c_12() #cklt#(#GT()) -> c_13() #cklt#(#LT()) -> c_14() #compare#(#0(),#0()) -> c_15() #compare#(#0(),#neg(@y)) -> c_16() #compare#(#0(),#pos(@y)) -> c_17() #compare#(#0(),#s(@y)) -> c_18() #compare#(#neg(@x),#0()) -> c_19() #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_21() #compare#(#pos(@x),#0()) -> c_22() #compare#(#pos(@x),#neg(@y)) -> c_23() #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_25() #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)) #less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) findMin#1#(nil()) -> c_4() findMin#2#(nil(),@x) -> c_6() findMin#3#(#false(),@x,@y,@ys) -> c_7() findMin#3#(#true(),@x,@y,@ys) -> c_8() minSort#1#(nil()) -> c_11() - 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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort(@l) -> minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) -> ::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,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_2(findMin#1#(@l)) 2: findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)) 3: findMin#2#(::(@y,@ys),@x) -> c_5(findMin#3#(#less(@x,@y),@x,@y,@ys),#less#(@x,@y)) 4: minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) 5: minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) 6: #cklt#(#EQ()) -> c_12() 7: #cklt#(#GT()) -> c_13() 8: #cklt#(#LT()) -> c_14() 9: #compare#(#0(),#0()) -> c_15() 10: #compare#(#0(),#neg(@y)) -> c_16() 11: #compare#(#0(),#pos(@y)) -> c_17() 12: #compare#(#0(),#s(@y)) -> c_18() 13: #compare#(#neg(@x),#0()) -> c_19() 14: #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)) 15: #compare#(#neg(@x),#pos(@y)) -> c_21() 16: #compare#(#pos(@x),#0()) -> c_22() 17: #compare#(#pos(@x),#neg(@y)) -> c_23() 18: #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)) 19: #compare#(#s(@x),#0()) -> c_25() 20: #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)) 21: #less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) 22: findMin#1#(nil()) -> c_4() 23: findMin#2#(nil(),@x) -> c_6() 24: findMin#3#(#false(),@x,@y,@ys) -> c_7() 25: findMin#3#(#true(),@x,@y,@ys) -> c_8() 26: minSort#1#(nil()) -> c_11() * Step 4: RemoveWeakSuffixes WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)) minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) - Weak DPs: #cklt#(#EQ()) -> c_12() #cklt#(#GT()) -> c_13() #cklt#(#LT()) -> c_14() #compare#(#0(),#0()) -> c_15() #compare#(#0(),#neg(@y)) -> c_16() #compare#(#0(),#pos(@y)) -> c_17() #compare#(#0(),#s(@y)) -> c_18() #compare#(#neg(@x),#0()) -> c_19() #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)) #compare#(#neg(@x),#pos(@y)) -> c_21() #compare#(#pos(@x),#0()) -> c_22() #compare#(#pos(@x),#neg(@y)) -> c_23() #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)) #compare#(#s(@x),#0()) -> c_25() #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)) #less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) findMin#1#(nil()) -> c_4() findMin#2#(::(@y,@ys),@x) -> c_5(findMin#3#(#less(@x,@y),@x,@y,@ys),#less#(@x,@y)) findMin#2#(nil(),@x) -> c_6() findMin#3#(#false(),@x,@y,@ys) -> c_7() findMin#3#(#true(),@x,@y,@ys) -> c_8() minSort#1#(nil()) -> c_11() - 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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort(@l) -> minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) -> ::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,nil} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:findMin#(@l) -> c_2(findMin#1#(@l)) -->_1 findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)):2 -->_1 findMin#1#(nil()) -> c_4():21 2:S:findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)) -->_1 findMin#2#(::(@y,@ys),@x) -> c_5(findMin#3#(#less(@x,@y),@x,@y,@ys),#less#(@x,@y)):22 -->_1 findMin#2#(nil(),@x) -> c_6():23 -->_2 findMin#(@l) -> c_2(findMin#1#(@l)):1 3:S:minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) -->_1 minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)):4 -->_1 minSort#1#(nil()) -> c_11():26 -->_2 findMin#(@l) -> c_2(findMin#1#(@l)):1 4:S:minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) -->_1 minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)):3 5:W:#cklt#(#EQ()) -> c_12() 6:W:#cklt#(#GT()) -> c_13() 7:W:#cklt#(#LT()) -> c_14() 8:W:#compare#(#0(),#0()) -> c_15() 9:W:#compare#(#0(),#neg(@y)) -> c_16() 10:W:#compare#(#0(),#pos(@y)) -> c_17() 11:W:#compare#(#0(),#s(@y)) -> c_18() 12:W:#compare#(#neg(@x),#0()) -> c_19() 13:W:#compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)) -->_1 #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)):19 -->_1 #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)):17 -->_1 #compare#(#s(@x),#0()) -> c_25():18 -->_1 #compare#(#pos(@x),#neg(@y)) -> c_23():16 -->_1 #compare#(#pos(@x),#0()) -> c_22():15 -->_1 #compare#(#neg(@x),#pos(@y)) -> c_21():14 -->_1 #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)):13 -->_1 #compare#(#neg(@x),#0()) -> c_19():12 -->_1 #compare#(#0(),#s(@y)) -> c_18():11 -->_1 #compare#(#0(),#pos(@y)) -> c_17():10 -->_1 #compare#(#0(),#neg(@y)) -> c_16():9 -->_1 #compare#(#0(),#0()) -> c_15():8 14:W:#compare#(#neg(@x),#pos(@y)) -> c_21() 15:W:#compare#(#pos(@x),#0()) -> c_22() 16:W:#compare#(#pos(@x),#neg(@y)) -> c_23() 17:W:#compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)) -->_1 #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)):19 -->_1 #compare#(#s(@x),#0()) -> c_25():18 -->_1 #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)):17 -->_1 #compare#(#pos(@x),#neg(@y)) -> c_23():16 -->_1 #compare#(#pos(@x),#0()) -> c_22():15 -->_1 #compare#(#neg(@x),#pos(@y)) -> c_21():14 -->_1 #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)):13 -->_1 #compare#(#neg(@x),#0()) -> c_19():12 -->_1 #compare#(#0(),#s(@y)) -> c_18():11 -->_1 #compare#(#0(),#pos(@y)) -> c_17():10 -->_1 #compare#(#0(),#neg(@y)) -> c_16():9 -->_1 #compare#(#0(),#0()) -> c_15():8 18:W:#compare#(#s(@x),#0()) -> c_25() 19:W:#compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)) -->_1 #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)):19 -->_1 #compare#(#s(@x),#0()) -> c_25():18 -->_1 #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)):17 -->_1 #compare#(#pos(@x),#neg(@y)) -> c_23():16 -->_1 #compare#(#pos(@x),#0()) -> c_22():15 -->_1 #compare#(#neg(@x),#pos(@y)) -> c_21():14 -->_1 #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)):13 -->_1 #compare#(#neg(@x),#0()) -> c_19():12 -->_1 #compare#(#0(),#s(@y)) -> c_18():11 -->_1 #compare#(#0(),#pos(@y)) -> c_17():10 -->_1 #compare#(#0(),#neg(@y)) -> c_16():9 -->_1 #compare#(#0(),#0()) -> c_15():8 20:W:#less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) -->_2 #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)):19 -->_2 #compare#(#s(@x),#0()) -> c_25():18 -->_2 #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)):17 -->_2 #compare#(#pos(@x),#neg(@y)) -> c_23():16 -->_2 #compare#(#pos(@x),#0()) -> c_22():15 -->_2 #compare#(#neg(@x),#pos(@y)) -> c_21():14 -->_2 #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)):13 -->_2 #compare#(#neg(@x),#0()) -> c_19():12 -->_2 #compare#(#0(),#s(@y)) -> c_18():11 -->_2 #compare#(#0(),#pos(@y)) -> c_17():10 -->_2 #compare#(#0(),#neg(@y)) -> c_16():9 -->_2 #compare#(#0(),#0()) -> c_15():8 -->_1 #cklt#(#LT()) -> c_14():7 -->_1 #cklt#(#GT()) -> c_13():6 -->_1 #cklt#(#EQ()) -> c_12():5 21:W:findMin#1#(nil()) -> c_4() 22:W:findMin#2#(::(@y,@ys),@x) -> c_5(findMin#3#(#less(@x,@y),@x,@y,@ys),#less#(@x,@y)) -->_1 findMin#3#(#true(),@x,@y,@ys) -> c_8():25 -->_1 findMin#3#(#false(),@x,@y,@ys) -> c_7():24 -->_2 #less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)):20 23:W:findMin#2#(nil(),@x) -> c_6() 24:W:findMin#3#(#false(),@x,@y,@ys) -> c_7() 25:W:findMin#3#(#true(),@x,@y,@ys) -> c_8() 26:W:minSort#1#(nil()) -> c_11() 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_11() 21: findMin#1#(nil()) -> c_4() 23: findMin#2#(nil(),@x) -> c_6() 22: findMin#2#(::(@y,@ys),@x) -> c_5(findMin#3#(#less(@x,@y),@x,@y,@ys),#less#(@x,@y)) 20: #less#(@x,@y) -> c_1(#cklt#(#compare(@x,@y)),#compare#(@x,@y)) 5: #cklt#(#EQ()) -> c_12() 6: #cklt#(#GT()) -> c_13() 7: #cklt#(#LT()) -> c_14() 19: #compare#(#s(@x),#s(@y)) -> c_26(#compare#(@x,@y)) 17: #compare#(#pos(@x),#pos(@y)) -> c_24(#compare#(@x,@y)) 13: #compare#(#neg(@x),#neg(@y)) -> c_20(#compare#(@y,@x)) 8: #compare#(#0(),#0()) -> c_15() 9: #compare#(#0(),#neg(@y)) -> c_16() 10: #compare#(#0(),#pos(@y)) -> c_17() 11: #compare#(#0(),#s(@y)) -> c_18() 12: #compare#(#neg(@x),#0()) -> c_19() 14: #compare#(#neg(@x),#pos(@y)) -> c_21() 15: #compare#(#pos(@x),#0()) -> c_22() 16: #compare#(#pos(@x),#neg(@y)) -> c_23() 18: #compare#(#s(@x),#0()) -> c_25() 24: findMin#3#(#false(),@x,@y,@ys) -> c_7() 25: findMin#3#(#true(),@x,@y,@ys) -> c_8() * Step 5: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)) minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort(@l) -> minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) -> ::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/2,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:findMin#(@l) -> c_2(findMin#1#(@l)) -->_1 findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)):2 2:S:findMin#1#(::(@x,@xs)) -> c_3(findMin#2#(findMin(@xs),@x),findMin#(@xs)) -->_2 findMin#(@l) -> c_2(findMin#1#(@l)):1 3:S:minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) -->_1 minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)):4 -->_2 findMin#(@l) -> c_2(findMin#1#(@l)):1 4:S:minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) -->_1 minSort#(@l) -> c_9(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#(::(@x,@xs)) -> c_3(findMin#(@xs)) * Step 6: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) minSort(@l) -> minSort#1(findMin(@l)) minSort#1(::(@x,@xs)) -> ::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) * Step 7: DecomposeDG WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,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_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) and a lower component findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) Further, following extension rules are added to the lower component. minSort#(@l) -> findMin#(@l) minSort#(@l) -> minSort#1#(findMin(@l)) minSort#1#(::(@x,@xs)) -> minSort#(@xs) ** Step 7.a:1: SimplifyRHS WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,nil} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) -->_1 minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)):2 2:S:minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) -->_1 minSort#(@l) -> c_9(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_9(minSort#1#(findMin(@l))) ** Step 7.a:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: minSort#(@l) -> c_9(minSort#1#(findMin(@l))) minSort#1#(::(@x,@xs)) -> c_10(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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,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_9) = {1}, uargs(c_10) = {1} Following symbols are considered usable: all TcT has computed the following interpretation: p(#0) = [0] p(#EQ) = [6] p(#GT) = [6] p(#LT) = [6] p(#cklt) = [1] x1 + [0] p(#compare) = [6] p(#false) = [6] p(#less) = [6] p(#neg) = [0] p(#pos) = [0] p(#s) = [0] p(#true) = [6] p(::) = [1] x1 + [1] x2 + [3] p(findMin) = [1] x1 + [0] p(findMin#1) = [1] x1 + [0] p(findMin#2) = [1] x1 + [1] x2 + [3] 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 + [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) = [1] x1 + [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) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] Following rules are strictly oriented: minSort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [3] > [1] @xs + [0] = c_10(minSort#(@xs)) Following rules are (at-least) weakly oriented: minSort#(@l) = [1] @l + [0] >= [1] @l + [0] = c_9(minSort#1#(findMin(@l))) #cklt(#EQ()) = [6] >= [6] = #false() #cklt(#GT()) = [6] >= [6] = #false() #cklt(#LT()) = [6] >= [6] = #true() #compare(#0(),#0()) = [6] >= [6] = #EQ() #compare(#0(),#neg(@y)) = [6] >= [6] = #GT() #compare(#0(),#pos(@y)) = [6] >= [6] = #LT() #compare(#0(),#s(@y)) = [6] >= [6] = #LT() #compare(#neg(@x),#0()) = [6] >= [6] = #LT() #compare(#neg(@x),#neg(@y)) = [6] >= [6] = #compare(@y,@x) #compare(#neg(@x),#pos(@y)) = [6] >= [6] = #LT() #compare(#pos(@x),#0()) = [6] >= [6] = #GT() #compare(#pos(@x),#neg(@y)) = [6] >= [6] = #GT() #compare(#pos(@x),#pos(@y)) = [6] >= [6] = #compare(@x,@y) #compare(#s(@x),#0()) = [6] >= [6] = #GT() #compare(#s(@x),#s(@y)) = [6] >= [6] = #compare(@x,@y) #less(@x,@y) = [6] >= [6] = #cklt(#compare(@x,@y)) findMin(@l) = [1] @l + [0] >= [1] @l + [0] = findMin#1(@l) findMin#1(::(@x,@xs)) = [1] @x + [1] @xs + [3] >= [1] @x + [1] @xs + [3] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(::(@y,@ys),@x) = [1] @x + [1] @y + [1] @ys + [6] >= [1] @x + [1] @y + [1] @ys + [6] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [1] @x + [3] >= [1] @x + [3] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [6] >= [1] @x + [1] @y + [1] @ys + [6] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [6] >= [1] @x + [1] @y + [1] @ys + [6] = ::(@x,::(@y,@ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:3: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: minSort#(@l) -> c_9(minSort#1#(findMin(@l))) - Weak DPs: minSort#1#(::(@x,@xs)) -> c_10(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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,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_9) = {1}, uargs(c_10) = {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] p(#pos) = [0] p(#s) = [0] p(#true) = [2] p(::) = [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#) = [1] x2 + [4] p(findMin#3#) = [1] x1 + [4] x3 + [0] p(minSort#) = [1] x1 + [1] 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) = [1] x1 + [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) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] Following rules are strictly oriented: minSort#(@l) = [1] @l + [1] > [1] @l + [0] = c_9(minSort#1#(findMin(@l))) Following rules are (at-least) weakly oriented: minSort#1#(::(@x,@xs)) = [1] @x + [1] @xs + [1] >= [1] @xs + [1] = c_10(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(::(@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(::(@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] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2] >= [1] @x + [1] @y + [1] @ys + [2] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1] @x + [1] @y + [1] @ys + [2] >= [1] @x + [1] @y + [1] @ys + [2] = ::(@x,::(@y,@ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.a:4: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: minSort#(@l) -> c_9(minSort#1#(findMin(@l))) minSort#1#(::(@x,@xs)) -> c_10(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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/1,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 7.b:1: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) - Weak DPs: minSort#(@l) -> findMin#(@l) minSort#(@l) -> minSort#1#(findMin(@l)) minSort#1#(::(@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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,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_2) = {1}, uargs(c_3) = {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(::) = [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#) = [3] p(findMin#2#) = [0] p(findMin#3#) = [0] p(minSort#) = [0] p(minSort#1#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [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) = [0] p(c_23) = [0] p(c_24) = [1] x1 + [2] p(c_25) = [1] p(c_26) = [4] x1 + [2] Following rules are strictly oriented: findMin#1#(::(@x,@xs)) = [3] > [0] = c_3(findMin#(@xs)) Following rules are (at-least) weakly oriented: findMin#(@l) = [0] >= [3] = c_2(findMin#1#(@l)) minSort#(@l) = [0] >= [0] = findMin#(@l) minSort#(@l) = [0] >= [0] = minSort#1#(findMin(@l)) minSort#1#(::(@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(::(@x,@xs)) = [0] >= [0] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(::(@y,@ys),@x) = [0] >= [0] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [0] >= [0] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [0] >= [0] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [0] >= [0] = ::(@x,::(@y,@ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:2: WeightGap WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) - Weak DPs: findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) minSort#(@l) -> findMin#(@l) minSort#(@l) -> minSort#1#(findMin(@l)) minSort#1#(::(@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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,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_2) = {1}, uargs(c_3) = {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 + [1] p(#compare) = [0] p(#false) = [1] p(#less) = [1] p(#neg) = [1] p(#pos) = [1] x1 + [1] p(#s) = [4] p(#true) = [1] p(::) = [1] x2 + [4] p(findMin) = [1] x1 + [0] p(findMin#1) = [1] x1 + [0] p(findMin#2) = [1] x1 + [4] p(findMin#3) = [1] x1 + [1] x4 + [7] p(minSort) = [2] x1 + [1] p(minSort#1) = [1] x1 + [1] p(nil) = [0] p(#cklt#) = [0] p(#compare#) = [4] x1 + [1] p(#less#) = [2] x2 + [0] p(findMin#) = [1] x1 + [1] p(findMin#1#) = [1] x1 + [0] p(findMin#2#) = [1] x1 + [4] x2 + [1] p(findMin#3#) = [1] x4 + [2] p(minSort#) = [1] x1 + [1] p(minSort#1#) = [1] x1 + [1] p(c_1) = [4] x2 + [1] p(c_2) = [1] x1 + [0] p(c_3) = [1] x1 + [2] p(c_4) = [0] p(c_5) = [1] x1 + [4] p(c_6) = [4] p(c_7) = [4] p(c_8) = [0] p(c_9) = [1] x1 + [4] x2 + [0] p(c_10) = [0] p(c_11) = [4] p(c_12) = [0] p(c_13) = [1] p(c_14) = [0] p(c_15) = [0] p(c_16) = [1] p(c_17) = [2] p(c_18) = [4] p(c_19) = [2] p(c_20) = [4] x1 + [4] p(c_21) = [0] p(c_22) = [1] p(c_23) = [2] p(c_24) = [1] p(c_25) = [1] p(c_26) = [1] Following rules are strictly oriented: findMin#(@l) = [1] @l + [1] > [1] @l + [0] = c_2(findMin#1#(@l)) Following rules are (at-least) weakly oriented: findMin#1#(::(@x,@xs)) = [1] @xs + [4] >= [1] @xs + [3] = c_3(findMin#(@xs)) minSort#(@l) = [1] @l + [1] >= [1] @l + [1] = findMin#(@l) minSort#(@l) = [1] @l + [1] >= [1] @l + [1] = minSort#1#(findMin(@l)) minSort#1#(::(@x,@xs)) = [1] @xs + [5] >= [1] @xs + [1] = minSort#(@xs) #cklt(#EQ()) = [1] >= [1] = #false() #cklt(#GT()) = [1] >= [1] = #false() #cklt(#LT()) = [1] >= [1] = #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) = [1] >= [1] = #cklt(#compare(@x,@y)) findMin(@l) = [1] @l + [0] >= [1] @l + [0] = findMin#1(@l) findMin#1(::(@x,@xs)) = [1] @xs + [4] >= [1] @xs + [4] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(::(@y,@ys),@x) = [1] @ys + [8] >= [1] @ys + [8] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [4] >= [4] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1] @ys + [8] >= [1] @ys + [8] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1] @ys + [8] >= [1] @ys + [8] = ::(@x,::(@y,@ys)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. ** Step 7.b:3: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) minSort#(@l) -> findMin#(@l) minSort#(@l) -> minSort#1#(findMin(@l)) minSort#1#(::(@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(::(@x,@xs)) -> findMin#2(findMin(@xs),@x) findMin#1(nil()) -> nil() findMin#2(::(@y,@ys),@x) -> findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) -> ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) -> ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) -> ::(@x,::(@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,::/2,nil/0,c_1/2,c_2/1,c_3/1,c_4/0,c_5/2,c_6/0,c_7/0 ,c_8/0,c_9/2,c_10/1,c_11/0,c_12/0,c_13/0,c_14/0,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/1,c_21/0,c_22/0 ,c_23/0,c_24/1,c_25/0,c_26/1} - 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,::,nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))