WORST_CASE(?,O(n^2)) * Step 1: Ara 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: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = Z3} + Details: Signatures used: ---------------- #0 :: [] -(0)-> A(0, 0) #EQ :: [] -(0)-> A(3, 3) #EQ :: [] -(0)-> A(10, 10) #GT :: [] -(0)-> A(3, 3) #GT :: [] -(0)-> A(10, 10) #LT :: [] -(0)-> A(3, 3) #LT :: [] -(0)-> A(10, 10) #cklt :: [A(3, 3)] -(0)-> A(15, 15) #compare :: [A(0, 0) x A(0, 0)] -(0)-> A(4, 4) #false :: [] -(0)-> A(0, 0) #false :: [] -(0)-> A(15, 15) #less :: [A(0, 0) x A(0, 0)] -(1)-> A(13, 13) #neg :: [A(0, 0)] -(0)-> A(0, 0) #pos :: [A(0, 0)] -(0)-> A(0, 0) #s :: [A(0, 0)] -(0)-> A(0, 0) #true :: [] -(0)-> A(0, 0) #true :: [] -(0)-> A(15, 15) :: :: [A(0, 0) x A(11, 6)] -(5)-> A(5, 6) :: :: [A(0, 0) x A(12, 6)] -(6)-> A(6, 6) :: :: [A(0, 0) x A(10, 6)] -(4)-> A(4, 6) :: :: [A(0, 0) x A(10, 10)] -(0)-> A(0, 10) :: :: [A(0, 0) x A(6, 6)] -(0)-> A(0, 6) :: :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) findMin :: [A(9, 6)] -(2)-> A(4, 6) findMin#1 :: [A(5, 6)] -(1)-> A(0, 6) findMin#2 :: [A(6, 6) x A(0, 0)] -(3)-> A(0, 6) findMin#3 :: [A(0, 0) x A(0, 0) x A(0, 0) x A(12, 6)] -(7)-> A(0, 6) minSort :: [A(10, 6)] -(6)-> A(0, 0) minSort#1 :: [A(4, 6)] -(3)-> A(0, 0) nil :: [] -(0)-> A(5, 6) nil :: [] -(0)-> A(6, 6) nil :: [] -(0)-> A(4, 6) nil :: [] -(0)-> A(7, 13) nil :: [] -(0)-> A(15, 13) nil :: [] -(0)-> A(7, 7) Cost-free Signatures used: -------------------------- #0 :: [] -(0)-> A_cf(0, 0) #EQ :: [] -(0)-> A_cf(0, 0) #EQ :: [] -(0)-> A_cf(14, 14) #GT :: [] -(0)-> A_cf(0, 0) #GT :: [] -(0)-> A_cf(14, 14) #GT :: [] -(0)-> A_cf(14, 12) #LT :: [] -(0)-> A_cf(0, 0) #LT :: [] -(0)-> A_cf(14, 14) #cklt :: [A_cf(0, 0)] -(0)-> A_cf(11, 11) #cklt :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #compare :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) #compare :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #false :: [] -(0)-> A_cf(3, 3) #false :: [] -(0)-> A_cf(11, 11) #false :: [] -(0)-> A_cf(0, 0) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 8) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #neg :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #pos :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #true :: [] -(0)-> A_cf(3, 3) #true :: [] -(0)-> A_cf(11, 11) #true :: [] -(0)-> A_cf(0, 0) :: :: [A_cf(0, 0) x A_cf(4, 0)] -(4)-> A_cf(4, 0) :: :: [A_cf(0, 0) x A_cf(13, 9)] -(4)-> A_cf(4, 9) :: :: [A_cf(0, 0) x A_cf(2, 0)] -(2)-> A_cf(2, 0) :: :: [A_cf(0, 0) x A_cf(6, 4)] -(2)-> A_cf(2, 4) :: :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) findMin :: [A_cf(4, 0)] -(0)-> A_cf(4, 0) findMin :: [A_cf(2, 0)] -(0)-> A_cf(2, 0) findMin :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) findMin#1 :: [A_cf(4, 0)] -(0)-> A_cf(4, 0) findMin#1 :: [A_cf(2, 0)] -(0)-> A_cf(2, 0) findMin#1 :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) findMin#2 :: [A_cf(4, 0) x A_cf(0, 0)] -(4)-> A_cf(4, 0) findMin#2 :: [A_cf(2, 0) x A_cf(0, 0)] -(2)-> A_cf(2, 0) findMin#2 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) findMin#3 :: [A_cf(3, 3) x A_cf(0, 0) x A_cf(0, 0) x A_cf(4, 0)] -(8)-> A_cf(4, 0) findMin#3 :: [A_cf(3, 3) x A_cf(0, 0) x A_cf(0, 0) x A_cf(2, 0)] -(4)-> A_cf(2, 0) findMin#3 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) minSort :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) minSort#1 :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) nil :: [] -(0)-> A_cf(4, 0) nil :: [] -(0)-> A_cf(15, 11) nil :: [] -(0)-> A_cf(7, 3) nil :: [] -(0)-> A_cf(2, 0) nil :: [] -(0)-> A_cf(2, 2) nil :: [] -(0)-> A_cf(0, 0) Base Constructor Signatures used: --------------------------------- #0_A :: [] -(0)-> A(0) #EQ_A :: [] -(0)-> A(0) #GT_A :: [] -(0)-> A(0) #LT_A :: [] -(0)-> A(0) #false_A :: [] -(0)-> A(0) #neg_A :: [A(0)] -(0)-> A(0) #pos_A :: [A(0)] -(0)-> A(0) #s_A :: [A(0)] -(0)-> A(0) #true_A :: [] -(0)-> A(0) ::_A :: [A(0) x A(0)] -(0)-> A(0) nil_A :: [] -(0)-> A(1, 0) nil_A :: [] -(0)-> A(0, 1) * Step 2: Open MAYBE - 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} Following problems could not be solved: - 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} WORST_CASE(?,O(n^2))