(VAR
    key key1 keyX l l1 ls pivot rs valX vals vals1 x x'1 x'2 xs y y'1 y'2 ys z zs)

(DATATYPES
   a = < #false, #true >
   b = µX. < dd(X,X), nil, tuple#2(X,X), #0, #neg(X), #pos(X), #s(X) >
   c = < #EQ, #GT, #LT >
 )

(SIGNATURES
   #equal :: b x b -> a
   #eq :: b x b -> a
   #greater :: b x b -> a
   #compare :: b x b -> c
   #ckgt :: c -> a
   append :: b x b -> b
   append#1 :: b x b -> b
   insert :: b x b -> b
   insert#1 :: b x b x b -> b
   insert#2 :: b x b x b x b -> b
   insert#3 :: b x b x b x b x b -> b
   insert#4 :: a x b x b x b x b x b -> b
   quicksort :: b -> b
   quicksort#1 :: b -> b
   splitqs :: b x b -> b
   quicksort#2 :: b x b -> b
   sortAll :: b -> b
   sortAll#1 :: b -> b
   sortAll#2 :: b x b -> b
   split :: b -> b
   split#1 :: b -> b
   splitAndSort :: b -> b
   splitqs#1 :: b x b -> b
   splitqs#2 :: b x b x b -> b
   splitqs#3 :: a x b x b x b -> b
   #and :: a x a -> a
 )

(RULES
    #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))
    #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)))