(STARTTERM
    CONSTRUCTOR-BASED)
(STRATEGY
    INNERMOST)

(VAR
    @dir @direction @h @hi @l @l' @l1 @l2 @low @n @n' @s @s1 @s2 @x @x1 @x2 @xs @xs' @y @ys @zipWithAnd@3 @zipWithAnd@4 @zipWithOr@1 @zipWithOr@2)
(RULES
    +(@x,@y) -> #add(@x,@y)
    and(@x,@y) -> #and(@x,@y)
    append(@l,@ys) -> append#1(@l,@ys)
    append#1(::(@x,@xs),@ys) -> append#2(append(@xs,@ys),@x)
    append#1(nil(),@ys) -> @ys
    append#2(@l',@x) -> ::(@x,@l')
    bitonicMerge(@l,@direction) -> bitonicMerge#1(@l,@direction,@l)
    bitonicMerge#1(::(@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(::(@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(@zipWithOr@1,@zipWithOr@2)) -> zipWithOr(@zipWithOr@1,@zipWithOr@2)
    bitonicMerge#7(@low,@direction,@hi) -> bitonicMerge#9(bitonicMerge#10(@direction,@hi,@low),@direction)
    bitonicMerge#8(tuple#2(@zipWithAnd@3,@zipWithAnd@4)) -> zipWithAnd(@zipWithAnd@3,@zipWithAnd@4)
    bitonicMerge#9(tuple#2(@hi,@low),@direction) -> append(bitonicMerge(@low,@direction),bitonicMerge(@hi,@direction))
    bitonicSort(@l,@dir) -> bitonicSort#1(@l,@dir,@l)
    bitonicSort#1(::(@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)) -> +(#pos(#s(#0())),div2(@n))
    length(@l) -> length#1(@l)
    length#1(::(@x,@xs)) -> +(#pos(#s(#0())),length(@xs))
    length#1(nil()) -> #0()
    or(@x,@y) -> #or(@x,@y)
    split(@l) -> split#1(@l)
    split#1(::(@x1,@xs)) -> split#2(@xs,@x1)
    split#1(nil()) -> tuple#2(nil(),nil())
    split#2(::(@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(::(@x1,@l1),::(@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(::(@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(::(@x,@l1),@l2)
    zipWithAnd(@l1,@l2) -> zipWithAnd#1(@l1,@l2)
    zipWithAnd#1(::(@x,@xs),@l2) -> zipWithAnd#2(@l2,@x,@xs)
    zipWithAnd#1(nil(),@l2) -> nil()
    zipWithAnd#2(::(@y,@ys),@x,@xs) -> ::(and(@x,@y),zipWithAnd(@xs,@ys))
    zipWithAnd#2(nil(),@x,@xs) -> nil()
    zipWithOr(@l1,@l2) -> zipWithOr#1(@l1,@l2)
    zipWithOr#1(::(@x,@xs),@l2) -> zipWithOr#2(@l2,@x,@xs)
    zipWithOr#1(nil(),@l2) -> nil()
    zipWithOr#2(::(@y,@ys),@x,@xs) -> ::(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))))
(COMMENT
    This TRS was automatically generated from the resource aware ML program 'bitonic.raml', c.f. http://raml.tcs.ifi.lmu.de/)