(VAR
    dir direction h hi l l' l1 l2 low n n' s s1 s2 x x1 x2 xs xs' y ys zipWithAnd3 zipWithAnd4 zipWithOr1 zipWithOr2)

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

(SIGNATURES
   add :: a x a -> a
   #add :: a x a -> a
   and :: c x c -> c
   #and :: c x c -> c
   append :: d x d -> d
   append#1 :: d x d -> d
   append#2 :: d x c -> d
   bitonicMerge :: d x c -> d
   bitonicMerge#1 :: d x c x d -> d
   bitonicMerge#2 :: d x c x d -> d
   bitonicMerge#10 :: c x d x d -> b
   length :: d -> a
   div2 :: a -> a
   bitonicMerge#3 :: a x c x d -> d
   splitAt :: a x d -> b
   bitonicMerge#4 :: b x c -> d
   bitonicMerge#6 :: b -> d
   bitonicMerge#5 :: d x c x b -> d
   bitonicMerge#8 :: b -> d
   bitonicMerge#7 :: d x c x d -> d
   zipWithOr :: d x d -> d
   bitonicMerge#9 :: b x c -> d
   zipWithAnd :: d x d -> d
   bitonicSort :: d x c -> d
   bitonicSort#1 :: d x c x d -> d
   split :: d -> b
   bitonicSort#2 :: b x c -> d
   bitonicSort#3 :: d x c x d x d -> d
   bitonicSort#4 :: d x c x d x d -> d
   div2#1 :: a -> a
   div2#2 :: a -> a
   length#1 :: d -> a
   or :: c x c -> c
   #or :: c x c -> c
   split#1 :: d -> b
   split#2 :: d x c -> b
   split#3 :: b x c x c -> b
   splitAt#1 :: a x d -> b
   splitAt#2 :: d x a -> b
   splitAt#3 :: b x c -> b
   zipWithAnd#1 :: d x d -> d
   zipWithAnd#2 :: d x c x d -> d
   zipWithOr#1 :: d x d -> d
   zipWithOr#2 :: d x c x d -> d
   #pred :: a -> a
   #succ :: a -> a
 )

(RULES
    add(x,y) -> #add(x,y)
    and(x,y) -> #and(x,y)
    append(l,ys) -> append#1(l,ys)
    append#1(dd(x,xs),ys) -> append#2(append(xs,ys),x)
    append#1(nil,ys) -> ys
    append#2(l',x) -> dd(x,l')
    bitonicMerge(l,direction) -> bitonicMerge#1(l,direction,l)
    bitonicMerge#1(dd(x,xs),direction,l) -> bitonicMerge#2(xs,direction,l)
    bitonicMerge#1(nil,direction,l) -> nil
    bitonicMerge#10(#false,hi,low) -> tuple#2(low,hi)
    bitonicMerge#10(#true,hi,low) -> tuple#2(hi,low)
    bitonicMerge#2(dd(y,ys),direction,l) -> bitonicMerge#3(div2(length(l)),direction,l)
    bitonicMerge#2(nil,direction,l) -> l
    bitonicMerge#3(h,direction,l) -> bitonicMerge#4(splitAt(h,l),direction)
    bitonicMerge#4(s,direction) -> bitonicMerge#5(bitonicMerge#6(s),direction,s)
    bitonicMerge#5(hi,direction,s) -> bitonicMerge#7(bitonicMerge#8(s),direction,hi)
    bitonicMerge#6(tuple#2(zipWithOr1,zipWithOr2)) -> zipWithOr(zipWithOr1,zipWithOr2)
    bitonicMerge#7(low,direction,hi) -> bitonicMerge#9(bitonicMerge#10(direction,hi,low),direction)
    bitonicMerge#8(tuple#2(zipWithAnd3,zipWithAnd4)) -> zipWithAnd(zipWithAnd3,zipWithAnd4)
    bitonicMerge#9(tuple#2(hi,low),direction) -> append(bitonicMerge(low,direction),bitonicMerge(hi,direction))
    bitonicSort(l,dir) -> bitonicSort#1(l,dir,l)
    bitonicSort#1(dd(x,xs),dir,l) -> bitonicSort#2(split(l),dir)
    bitonicSort#1(nil,dir,l) -> nil
    bitonicSort#2(tuple#2(l1,l2),dir) -> bitonicSort#3(bitonicSort(l1,#true),dir,l1,l2)
    bitonicSort#3(s1,dir,l1,l2) -> bitonicSort#4(bitonicSort(l2,#false),dir,l1,l2)
    bitonicSort#4(s2,dir,l1,l2) -> bitonicMerge(append(l1,l2),dir)
    div2(n) -> div2#1(n)
    div2#1(#0) -> #0
    div2#1(#s(n)) -> div2#2(n)
    div2#2(#0) -> #0
    div2#2(#s(n)) -> add(#pos(#s(#0)),div2(n))
    length(l) -> length#1(l)
    length#1(dd(x,xs)) -> add(#pos(#s(#0)),length(xs))
    length#1(nil) -> #0
    or(x,y) -> #or(x,y)
    split(l) -> split#1(l)
    split#1(dd(x1,xs)) -> split#2(xs,x1)
    split#1(nil) -> tuple#2(nil,nil)
    split#2(dd(x2,xs'),x1) -> split#3(split(xs'),x1,x2)
    split#2(nil,x1) -> tuple#2(nil,nil)
    split#3(tuple#2(l1,l2),x1,x2) -> tuple#2(dd(x1,l1),dd(x2,l2))
    splitAt(n,l) -> splitAt#1(n,l)
    splitAt#1(#0,l) -> tuple#2(nil,l)
    splitAt#1(#s(n'),l) -> splitAt#2(l,n')
    splitAt#2(dd(x,xs),n') -> splitAt#3(splitAt(n',xs),x)
    splitAt#2(nil,n') -> tuple#2(nil,nil)
    splitAt#3(tuple#2(l1,l2),x) -> tuple#2(dd(x,l1),l2)
    zipWithAnd(l1,l2) -> zipWithAnd#1(l1,l2)
    zipWithAnd#1(dd(x,xs),l2) -> zipWithAnd#2(l2,x,xs)
    zipWithAnd#1(nil,l2) -> nil
    zipWithAnd#2(dd(y,ys),x,xs) -> dd(and(x,y),zipWithAnd(xs,ys))
    zipWithAnd#2(nil,x,xs) -> nil
    zipWithOr(l1,l2) -> zipWithOr#1(l1,l2)
    zipWithOr#1(dd(x,xs),l2) -> zipWithOr#2(l2,x,xs)
    zipWithOr#1(nil,l2) -> nil
    zipWithOr#2(dd(y,ys),x,xs) -> dd(or(x,y),zipWithOr(xs,ys))
    zipWithOr#2(nil,x,xs) -> nil
    #add(#0,y) -> y
    #add(#neg(#s(#0)),y) -> #pred(y)
    #add(#neg(#s(#s(x))),y) -> #pred(#add(#pos(#s(x)),y))
    #add(#pos(#s(#0)),y) -> #succ(y)
    #add(#pos(#s(#s(x))),y) -> #succ(#add(#pos(#s(x)),y))
    #and(#false,#false) -> #false
    #and(#false,#true) -> #false
    #and(#true,#false) -> #false
    #and(#true,#true) -> #true
    #or(#false,#false) -> #false
    #or(#false,#true) -> #true
    #or(#true,#false) -> #true
    #or(#true,#true) -> #true
    #pred(#0) -> #neg(#s(#0))
    #pred(#neg(#s(x))) -> #neg(#s(#s(x)))
    #pred(#pos(#s(#0))) -> #0
    #pred(#pos(#s(#s(x)))) -> #pos(#s(x))
    #succ(#0) -> #pos(#s(#0))
    #succ(#neg(#s(#0))) -> #0
    #succ(#neg(#s(#s(x)))) -> #neg(#s(x))
    #succ(#pos(#s(x))) -> #pos(#s(#s(x))))