WORST_CASE(?,O(n^2)) * Step 1: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #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) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2} / {#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 {#and,#cklt,#compare,#eq,#equal,#less,#or,and,insert ,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or} 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) #and :: [A(1, 1) x A(1, 1)] -(0)-> A(12, 4) #cklt :: [A(3, 3)] -(0)-> A(7, 7) #compare :: [A(0, 0) x A(0, 0)] -(0)-> A(4, 4) #eq :: [A(0, 0) x A(0, 0)] -(0)-> A(12, 4) #equal :: [A(0, 0) x A(1, 0)] -(1)-> A(11, 3) #false :: [] -(0)-> A(0, 1) #false :: [] -(0)-> A(1, 1) #false :: [] -(0)-> A(7, 0) #false :: [] -(0)-> A(15, 15) #false :: [] -(0)-> A(15, 11) #false :: [] -(0)-> A(13, 13) #less :: [A(0, 0) x A(2, 0)] -(1)-> A(7, 7) #neg :: [A(0, 0)] -(0)-> A(0, 0) #or :: [A(1, 1) x A(7, 0)] -(0)-> A(15, 15) #pos :: [A(0, 0)] -(0)-> A(0, 0) #s :: [A(0, 0)] -(0)-> A(0, 0) #true :: [] -(0)-> A(0, 1) #true :: [] -(0)-> A(1, 1) #true :: [] -(0)-> A(7, 0) #true :: [] -(0)-> A(15, 15) #true :: [] -(0)-> A(15, 11) #true :: [] -(0)-> A(13, 13) :: :: [A(7, 0) x A(7, 0)] -(7)-> A(7, 0) :: :: [A(7, 0) x A(15, 8)] -(7)-> A(7, 8) :: :: [A(0, 0) x A(0, 0)] -(0)-> A(0, 0) :: :: [A(1, 0) x A(7, 6)] -(1)-> A(1, 6) and :: [A(9, 1) x A(12, 12)] -(1)-> A(12, 4) insert :: [A(6, 0) x A(7, 0)] -(4)-> A(0, 0) insert#1 :: [A(7, 0) x A(6, 0)] -(3)-> A(0, 0) insert#2 :: [A(0, 1) x A(6, 0) x A(0, 0) x A(7, 0)] -(5)-> A(0, 0) isortlist :: [A(15, 8)] -(4)-> A(7, 0) isortlist#1 :: [A(7, 8)] -(3)-> A(0, 0) leq :: [A(0, 0) x A(7, 0)] -(3)-> A(9, 10) leq#1 :: [A(0, 0) x A(7, 0)] -(2)-> A(8, 9) leq#2 :: [A(7, 0) x A(0, 0) x A(0, 0)] -(1)-> A(8, 8) nil :: [] -(0)-> A(7, 0) nil :: [] -(0)-> A(7, 8) nil :: [] -(0)-> A(0, 0) nil :: [] -(0)-> A(15, 15) nil :: [] -(0)-> A(7, 7) or :: [A(1, 1) x A(8, 0)] -(1)-> A(13, 13) 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) #LT :: [] -(0)-> A_cf(0, 0) #LT :: [] -(0)-> A_cf(14, 14) #and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #and :: [A_cf(3, 0) x A_cf(3, 3)] -(0)-> A_cf(10, 8) #and :: [A_cf(7, 0) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #and :: [A_cf(0, 1) x A_cf(0, 1)] -(0)-> A_cf(14, 14) #and :: [A_cf(7, 7) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 14) #and :: [A_cf(0, 7) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #and :: [A_cf(3, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 14) #and :: [A_cf(3, 0) x A_cf(3, 4)] -(0)-> A_cf(14, 14) #and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 8) #cklt :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #cklt :: [A_cf(0, 0)] -(0)-> A_cf(15, 15) #compare :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #compare :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(10, 8) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 10) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(11, 12) #eq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 8) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(4, 8) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(9, 4) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(10, 10) #equal :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(4, 9) #false :: [] -(0)-> A_cf(0, 0) #false :: [] -(0)-> A_cf(0, 1) #false :: [] -(0)-> A_cf(15, 15) #false :: [] -(0)-> A_cf(11, 11) #false :: [] -(0)-> A_cf(3, 0) #false :: [] -(0)-> A_cf(3, 3) #false :: [] -(0)-> A_cf(1, 3) #false :: [] -(0)-> A_cf(7, 0) #false :: [] -(0)-> A_cf(15, 11) #false :: [] -(0)-> A_cf(7, 7) #false :: [] -(0)-> A_cf(11, 15) #false :: [] -(0)-> A_cf(0, 7) #false :: [] -(0)-> A_cf(11, 14) #false :: [] -(0)-> A_cf(3, 4) #false :: [] -(0)-> A_cf(15, 14) #false :: [] -(0)-> A_cf(14, 14) #false :: [] -(0)-> A_cf(2, 10) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) #less :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 12) #neg :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #or :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) #or :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(15, 15) #pos :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #s :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) #true :: [] -(0)-> A_cf(0, 0) #true :: [] -(0)-> A_cf(0, 1) #true :: [] -(0)-> A_cf(15, 15) #true :: [] -(0)-> A_cf(11, 11) #true :: [] -(0)-> A_cf(3, 3) #true :: [] -(0)-> A_cf(3, 0) #true :: [] -(0)-> A_cf(1, 3) #true :: [] -(0)-> A_cf(7, 0) #true :: [] -(0)-> A_cf(15, 11) #true :: [] -(0)-> A_cf(7, 7) #true :: [] -(0)-> A_cf(0, 7) #true :: [] -(0)-> A_cf(11, 14) #true :: [] -(0)-> A_cf(3, 4) #true :: [] -(0)-> A_cf(15, 14) #true :: [] -(0)-> A_cf(14, 14) #true :: [] -(0)-> A_cf(2, 10) :: :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) :: :: [A_cf(0, 0) x A_cf(9, 9)] -(0)-> A_cf(0, 9) :: :: [A_cf(8, 0) x A_cf(8, 0)] -(8)-> A_cf(8, 0) :: :: [A_cf(7, 0) x A_cf(7, 0)] -(7)-> A_cf(7, 0) :: :: [A_cf(7, 0) x A_cf(15, 8)] -(7)-> A_cf(7, 8) and :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) and :: [A_cf(4, 4) x A_cf(12, 9)] -(0)-> A_cf(12, 12) and :: [A_cf(8, 4) x A_cf(8, 8)] -(0)-> A_cf(12, 12) and :: [A_cf(8, 8) x A_cf(0, 0)] -(0)-> A_cf(12, 12) and :: [A_cf(0, 8) x A_cf(0, 0)] -(0)-> A_cf(12, 12) and :: [A_cf(4, 8) x A_cf(0, 4)] -(0)-> A_cf(12, 12) insert :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) insert :: [A_cf(8, 0) x A_cf(7, 0)] -(7)-> A_cf(7, 0) insert#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) insert#1 :: [A_cf(7, 0) x A_cf(8, 0)] -(7)-> A_cf(7, 0) insert#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) insert#2 :: [A_cf(0, 1) x A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) insert#2 :: [A_cf(1, 3) x A_cf(8, 0) x A_cf(7, 0) x A_cf(7, 0)] -(14)-> A_cf(7, 0) isortlist :: [A_cf(8, 0)] -(0)-> A_cf(7, 0) isortlist :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) isortlist#1 :: [A_cf(8, 0)] -(0)-> A_cf(7, 0) isortlist#1 :: [A_cf(0, 0)] -(0)-> A_cf(0, 0) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 12) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(10, 10) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 1) leq :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(4, 4) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 12) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(1, 1) leq#1 :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 1) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(14, 14) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(12, 12) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(8, 15) leq#2 :: [A_cf(0, 0) x A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 1) nil :: [] -(0)-> A_cf(0, 0) nil :: [] -(0)-> A_cf(15, 11) nil :: [] -(0)-> A_cf(8, 0) nil :: [] -(0)-> A_cf(7, 0) nil :: [] -(0)-> A_cf(11, 2) or :: [A_cf(0, 0) x A_cf(0, 0)] -(0)-> A_cf(0, 0) or :: [A_cf(4, 4) x A_cf(4, 4)] -(0)-> A_cf(14, 14) or :: [A_cf(4, 4) x A_cf(4, 4)] -(0)-> A_cf(12, 12) or :: [A_cf(4, 4) x A_cf(4, 4)] -(0)-> A_cf(14, 15) 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: #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #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) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2} / {#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 {#and,#cklt,#compare,#eq,#equal,#less,#or,and,insert ,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or} and constructors {#0,#EQ,#GT,#LT,#false,#neg ,#pos,#s,#true,::,nil} Following problems could not be solved: - Strict TRS: #equal(@x,@y) -> #eq(@x,@y) #less(@x,@y) -> #cklt(#compare(@x,@y)) and(@x,@y) -> #and(@x,@y) insert(@x,@l) -> insert#1(@l,@x) insert#1(::(@y,@ys),@x) -> insert#2(leq(@x,@y),@x,@y,@ys) insert#1(nil(),@x) -> ::(@x,nil()) insert#2(#false(),@x,@y,@ys) -> ::(@y,insert(@x,@ys)) insert#2(#true(),@x,@y,@ys) -> ::(@x,::(@y,@ys)) isortlist(@l) -> isortlist#1(@l) isortlist#1(::(@x,@xs)) -> insert(@x,isortlist(@xs)) isortlist#1(nil()) -> nil() leq(@l1,@l2) -> leq#1(@l1,@l2) leq#1(::(@x,@xs),@l2) -> leq#2(@l2,@x,@xs) leq#1(nil(),@l2) -> #true() leq#2(::(@y,@ys),@x,@xs) -> or(#less(@x,@y),and(#equal(@x,@y),leq(@xs,@ys))) leq#2(nil(),@x,@xs) -> #false() or(@x,@y) -> #or(@x,@y) - Weak TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #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) #eq(#0(),#0()) -> #true() #eq(#0(),#neg(@y)) -> #false() #eq(#0(),#pos(@y)) -> #false() #eq(#0(),#s(@y)) -> #false() #eq(#neg(@x),#0()) -> #false() #eq(#neg(@x),#neg(@y)) -> #eq(@x,@y) #eq(#neg(@x),#pos(@y)) -> #false() #eq(#pos(@x),#0()) -> #false() #eq(#pos(@x),#neg(@y)) -> #false() #eq(#pos(@x),#pos(@y)) -> #eq(@x,@y) #eq(#s(@x),#0()) -> #false() #eq(#s(@x),#s(@y)) -> #eq(@x,@y) #eq(::(@x_1,@x_2),::(@y_1,@y_2)) -> #and(#eq(@x_1,@y_1),#eq(@x_2,@y_2)) #eq(::(@x_1,@x_2),nil()) -> #false() #eq(nil(),::(@y_1,@y_2)) -> #false() #eq(nil(),nil()) -> #true() #or(#false(),#false()) -> #false() #or(#false(),#true()) -> #true() #or(#true(),#false()) -> #true() #or(#true(),#true()) -> #true() - Signature: {#and/2,#cklt/1,#compare/2,#eq/2,#equal/2,#less/2,#or/2,and/2,insert/2,insert#1/2,insert#2/4,isortlist/1 ,isortlist#1/1,leq/2,leq#1/2,leq#2/3,or/2} / {#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 {#and,#cklt,#compare,#eq,#equal,#less,#or,and,insert ,insert#1,insert#2,isortlist,isortlist#1,leq,leq#1,leq#2,or} and constructors {#0,#EQ,#GT,#LT,#false,#neg ,#pos,#s,#true,::,nil} WORST_CASE(?,O(n^2))