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: UsableRules 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: 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)) #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#(@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() * Step 3: 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)) - 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 4: 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)) - 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 5: 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)) - 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 6: 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)) - 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 7: Decompose 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: Decompose {onSelection = all cycle independent sub-graph, withBound = RelativeAdd} + Details: We analyse the complexity of following sub-problems (R) and (S). Problem (S) is obtained from the input problem by shifting strict rules from (R) into the weak component. Problem (R) - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) - Weak 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} Problem (S) - Strict DPs: minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) - Weak DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin(@l) -> findMin#1(@l) findMin#1(::(@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} ** Step 7.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) - Weak 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: findMin#(@l) -> c_2(findMin#1#(@l)) 2: findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) The strictly oriented rules are moved into the weak component. *** Step 7.a:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) - Weak 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: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_2) = {1}, uargs(c_3) = {1}, uargs(c_9) = {1,2}, uargs(c_10) = {1} Following symbols are considered usable: {findMin,findMin#1,findMin#2,findMin#3,#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#,findMin#3# ,minSort#,minSort#1#} TcT has computed the following interpretation: p(#0) = 0 p(#EQ) = 0 p(#GT) = 0 p(#LT) = 2 p(#cklt) = 0 p(#compare) = 2*x1*x2 p(#false) = 1 p(#less) = 0 p(#neg) = 1 + x1 p(#pos) = x1 p(#s) = x1 p(#true) = 2 p(::) = 1 + x1 + x2 p(findMin) = x1 p(findMin#1) = x1 p(findMin#2) = 1 + x1 + x2 p(findMin#3) = 2 + x2 + x3 + x4 p(minSort) = 2 + x1 + x1^2 p(minSort#1) = 2 + x1 + x1^2 p(nil) = 2 p(#cklt#) = 1 + 2*x1 + 2*x1^2 p(#compare#) = 1 + x1*x2 + 2*x2^2 p(#less#) = x1 + 2*x1*x2 + 2*x1^2 + 2*x2^2 p(findMin#) = 1 + 2*x1 p(findMin#1#) = 2*x1 p(findMin#2#) = 2*x1 + x1^2 + x2^2 p(findMin#3#) = 2*x2*x3 + x2*x4 + x2^2 + 2*x4 + 2*x4^2 p(minSort#) = 2 + 2*x1 + x1^2 p(minSort#1#) = 1 + x1^2 p(c_1) = x2 p(c_2) = x1 p(c_3) = x1 p(c_4) = 2 p(c_5) = 0 p(c_6) = 2 p(c_7) = 2 p(c_8) = 0 p(c_9) = x1 + x2 p(c_10) = x1 p(c_11) = 0 p(c_12) = 1 p(c_13) = 2 p(c_14) = 0 p(c_15) = 2 p(c_16) = 1 p(c_17) = 0 p(c_18) = 2 p(c_19) = 2 p(c_20) = 2 p(c_21) = 0 p(c_22) = 0 p(c_23) = 2 p(c_24) = 1 + x1 p(c_25) = 0 p(c_26) = 1 Following rules are strictly oriented: findMin#(@l) = 1 + 2*@l > 2*@l = c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) = 2 + 2*@x + 2*@xs > 1 + 2*@xs = c_3(findMin#(@xs)) Following rules are (at-least) weakly oriented: minSort#(@l) = 2 + 2*@l + @l^2 >= 2 + 2*@l + @l^2 = c_9(minSort#1#(findMin(@l)),findMin#(@l)) minSort#1#(::(@x,@xs)) = 2 + 2*@x + 2*@x*@xs + @x^2 + 2*@xs + @xs^2 >= 2 + 2*@xs + @xs^2 = c_10(minSort#(@xs)) findMin(@l) = @l >= @l = findMin#1(@l) findMin#1(::(@x,@xs)) = 1 + @x + @xs >= 1 + @x + @xs = findMin#2(findMin(@xs),@x) findMin#1(nil()) = 2 >= 2 = nil() findMin#2(::(@y,@ys),@x) = 2 + @x + @y + @ys >= 2 + @x + @y + @ys = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = 3 + @x >= 3 + @x = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = 2 + @x + @y + @ys >= 2 + @x + @y + @ys = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = 2 + @x + @y + @ys >= 2 + @x + @y + @ys = ::(@x,::(@y,@ys)) *** Step 7.a:1.a:2: Assumption 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) -> 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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 7.a:1.b:1: RemoveWeakSuffixes 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) -> 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:findMin#(@l) -> c_2(findMin#1#(@l)) -->_1 findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)):2 2:W:findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) -->_1 findMin#(@l) -> c_2(findMin#1#(@l)):1 3:W: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:W:minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) -->_1 minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) 4: minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) 1: findMin#(@l) -> c_2(findMin#1#(@l)) 2: findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) *** Step 7.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin(@l) -> findMin#1(@l) findMin#1(::(@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). ** Step 7.b:1: RemoveWeakSuffixes 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 DPs: findMin#(@l) -> c_2(findMin#1#(@l)) findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin(@l) -> findMin#1(@l) findMin#1(::(@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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:minSort#(@l) -> c_9(minSort#1#(findMin(@l)),findMin#(@l)) -->_2 findMin#(@l) -> c_2(findMin#1#(@l)):3 -->_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 3:W:findMin#(@l) -> c_2(findMin#1#(@l)) -->_1 findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)):4 4:W:findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) -->_1 findMin#(@l) -> c_2(findMin#1#(@l)):3 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: findMin#(@l) -> c_2(findMin#1#(@l)) 4: findMin#1#(::(@x,@xs)) -> c_3(findMin#(@xs)) ** Step 7.b:2: 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.b:3: PredecessorEstimationCP 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: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 2: minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) Consider the set of all dependency pairs 1: minSort#(@l) -> c_9(minSort#1#(findMin(@l))) 2: minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {2} These cover all (indirect) predecessors of dependency pairs {1,2} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. *** Step 7.b:3.a:1: NaturalMI 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: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_9) = {1}, uargs(c_10) = {1} Following symbols are considered usable: {findMin,findMin#1,findMin#2,findMin#3,#cklt#,#compare#,#less#,findMin#,findMin#1#,findMin#2#,findMin#3# ,minSort#,minSort#1#} TcT has computed the following interpretation: p(#0) = [2] p(#EQ) = [8] p(#GT) = [2] p(#LT) = [0] p(#cklt) = [1] x1 + [4] p(#compare) = [4] x1 + [6] x2 + [8] p(#false) = [0] p(#less) = [2] x2 + [1] p(#neg) = [1] x1 + [2] p(#pos) = [1] x1 + [0] p(#s) = [2] p(#true) = [0] p(::) = [1] x2 + [1] p(findMin) = [1] x1 + [0] p(findMin#1) = [1] x1 + [0] p(findMin#2) = [1] x1 + [1] p(findMin#3) = [1] x4 + [2] p(minSort) = [1] x1 + [1] p(minSort#1) = [1] x1 + [8] p(nil) = [0] p(#cklt#) = [1] p(#compare#) = [2] p(#less#) = [2] x1 + [2] x2 + [0] p(findMin#) = [0] p(findMin#1#) = [1] p(findMin#2#) = [1] x1 + [4] p(findMin#3#) = [1] x3 + [0] p(minSort#) = [8] x1 + [0] p(minSort#1#) = [8] x1 + [0] p(c_1) = [1] x1 + [2] x2 + [0] p(c_2) = [2] x1 + [4] p(c_3) = [1] x1 + [1] p(c_4) = [8] p(c_5) = [8] x1 + [8] x2 + [1] p(c_6) = [1] p(c_7) = [0] p(c_8) = [1] p(c_9) = [1] x1 + [0] p(c_10) = [1] x1 + [7] p(c_11) = [2] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [4] p(c_16) = [1] p(c_17) = [1] p(c_18) = [1] p(c_19) = [2] p(c_20) = [1] x1 + [1] p(c_21) = [0] p(c_22) = [1] p(c_23) = [1] p(c_24) = [1] p(c_25) = [1] p(c_26) = [2] Following rules are strictly oriented: minSort#1#(::(@x,@xs)) = [8] @xs + [8] > [8] @xs + [7] = c_10(minSort#(@xs)) Following rules are (at-least) weakly oriented: minSort#(@l) = [8] @l + [0] >= [8] @l + [0] = c_9(minSort#1#(findMin(@l))) findMin(@l) = [1] @l + [0] >= [1] @l + [0] = findMin#1(@l) findMin#1(::(@x,@xs)) = [1] @xs + [1] >= [1] @xs + [1] = findMin#2(findMin(@xs),@x) findMin#1(nil()) = [0] >= [0] = nil() findMin#2(::(@y,@ys),@x) = [1] @ys + [2] >= [1] @ys + [2] = findMin#3(#less(@x,@y),@x,@y,@ys) findMin#2(nil(),@x) = [1] >= [1] = ::(@x,nil()) findMin#3(#false(),@x,@y,@ys) = [1] @ys + [2] >= [1] @ys + [2] = ::(@y,::(@x,@ys)) findMin#3(#true(),@x,@y,@ys) = [1] @ys + [2] >= [1] @ys + [2] = ::(@x,::(@y,@ys)) *** Step 7.b:3.a:2: Assumption WORST_CASE(?,O(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: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 7.b:3.b:1: RemoveWeakSuffixes 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: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:minSort#(@l) -> c_9(minSort#1#(findMin(@l))) -->_1 minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)):2 2:W:minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) -->_1 minSort#(@l) -> c_9(minSort#1#(findMin(@l))):1 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: minSort#(@l) -> c_9(minSort#1#(findMin(@l))) 2: minSort#1#(::(@x,@xs)) -> c_10(minSort#(@xs)) *** Step 7.b:3.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: #cklt(#EQ()) -> #false() #cklt(#GT()) -> #false() #cklt(#LT()) -> #true() #compare(#0(),#0()) -> #EQ() #compare(#0(),#neg(@y)) -> #GT() #compare(#0(),#pos(@y)) -> #LT() #compare(#0(),#s(@y)) -> #LT() #compare(#neg(@x),#0()) -> #LT() #compare(#neg(@x),#neg(@y)) -> #compare(@y,@x) #compare(#neg(@x),#pos(@y)) -> #LT() #compare(#pos(@x),#0()) -> #GT() #compare(#pos(@x),#neg(@y)) -> #GT() #compare(#pos(@x),#pos(@y)) -> #compare(@x,@y) #compare(#s(@x),#0()) -> #GT() #compare(#s(@x),#s(@y)) -> #compare(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) findMin(@l) -> findMin#1(@l) findMin#1(::(@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). WORST_CASE(?,O(n^2))