MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict TRS: #and(#false(),#false()) -> #false() #and(#false(),#true()) -> #false() #and(#true(),#false()) -> #false() #and(#true(),#true()) -> #true() #ckgt(#EQ()) -> #false() #ckgt(#GT()) -> #true() #ckgt(#LT()) -> #false() #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(dd(x'1,x'2),dd(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #eq(dd(x'1,x'2),nil()) -> #false() #eq(dd(x'1,x'2),tuple#2(y'1,y'2)) -> #false() #eq(nil(),dd(y'1,y'2)) -> #false() #eq(nil(),nil()) -> #true() #eq(nil(),tuple#2(y'1,y'2)) -> #false() #eq(tuple#2(x'1,x'2),dd(y'1,y'2)) -> #false() #eq(tuple#2(x'1,x'2),nil()) -> #false() #eq(tuple#2(x'1,x'2),tuple#2(y'1,y'2)) -> #and(#eq(x'1,y'1),#eq(x'2,y'2)) #equal(x,y) -> #eq(x,y) #greater(x,y) -> #ckgt(#compare(x,y)) append(l,ys) -> append#1(l,ys) append#1(dd(x,xs),ys) -> dd(x,append(xs,ys)) append#1(nil(),ys) -> ys insert(x,l) -> insert#1(x,l,x) insert#1(tuple#2(valX,keyX),l,x) -> insert#2(l,keyX,valX,x) insert#2(dd(l1,ls),keyX,valX,x) -> insert#3(l1,keyX,ls,valX,x) insert#2(nil(),keyX,valX,x) -> dd(tuple#2(dd(valX,nil()),keyX),nil()) insert#3(tuple#2(vals1,key1),keyX,ls,valX,x) -> insert#4(#equal(key1,keyX),key1,ls,valX,vals1,x) insert#4(#false(),key1,ls,valX,vals1,x) -> dd(tuple#2(vals1,key1),insert(x,ls)) insert#4(#true(),key1,ls,valX,vals1,x) -> dd(tuple#2(dd(valX,vals1),key1),ls) quicksort(l) -> quicksort#1(l) quicksort#1(dd(z,zs)) -> quicksort#2(splitqs(z,zs),z) quicksort#1(nil()) -> nil() quicksort#2(tuple#2(xs,ys),z) -> append(quicksort(xs),dd(z,quicksort(ys))) sortAll(l) -> sortAll#1(l) sortAll#1(dd(x,xs)) -> sortAll#2(x,xs) sortAll#1(nil()) -> nil() sortAll#2(tuple#2(vals,key),xs) -> dd(tuple#2(quicksort(vals),key),sortAll(xs)) split(l) -> split#1(l) split#1(dd(x,xs)) -> insert(x,split(xs)) split#1(nil()) -> nil() splitAndSort(l) -> sortAll(split(l)) splitqs(pivot,l) -> splitqs#1(l,pivot) splitqs#1(dd(x,xs),pivot) -> splitqs#2(splitqs(pivot,xs),pivot,x) splitqs#1(nil(),pivot) -> tuple#2(nil(),nil()) splitqs#2(tuple#2(ls,rs),pivot,x) -> splitqs#3(#greater(x,pivot),ls,rs,x) splitqs#3(#false(),ls,rs,x) -> tuple#2(dd(x,ls),rs) splitqs#3(#true(),ls,rs,x) -> tuple#2(ls,dd(x,rs)) - Signature: {#and/2,#ckgt/1,#compare/2,#eq/2,#equal/2,#greater/2,append/2,append#1/2,insert/2,insert#1/3,insert#2/4 ,insert#3/5,insert#4/6,quicksort/1,quicksort#1/1,quicksort#2/2,sortAll/1,sortAll#1/1,sortAll#2/2,split/1 ,split#1/1,splitAndSort/1,splitqs/2,splitqs#1/2,splitqs#2/3,splitqs#3/4} / {#0/0,#EQ/0,#GT/0,#LT/0,#false/0 ,#neg/1,#pos/1,#s/1,#true/0,dd/2,nil/0,tuple#2/2} - Obligation: innermost runtime complexity wrt. defined symbols {#and,#ckgt,#compare,#eq,#equal,#greater,append,append#1 ,insert,insert#1,insert#2,insert#3,insert#4,quicksort,quicksort#1,quicksort#2,sortAll,sortAll#1,sortAll#2 ,split,split#1,splitAndSort,splitqs,splitqs#1,splitqs#2,splitqs#3} and constructors {#0,#EQ,#GT,#LT,#false ,#neg,#pos,#s,#true,dd,nil,tuple#2} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE