(STRATEGY
    INNERMOST)

(VAR
    @_@9 @a @b @breadth@1 @breadth@2
    @breadth@7 @breadth@8
    @children@3 @children@4
    @children@5 @children@6
    @copyover@1 @copyover@2
    @dequeue@1 @dequeue@2 @dequeue@3
    @dequeue@4 @elem @inq @l @l1 @l2
    @outq @queue @queue' @x @xs @y
    @ys @z)
(DATATYPES
    A = µX.< tuple#2(X, X), ::(X, X), nil, tuple#4(X, X, X, X), #unit >)
(SIGNATURES
    breadth :: [A x A] -> A
    breadth#1 :: [A] -> A
    breadth#2 :: [A x A] -> A
    breadth#3 :: [A x A] -> A
    breadth#4 :: [A] -> A
    breadth#5 :: [A] -> A
    children :: [A x A x A x A] -> A
    children#1 :: [A x A x A] -> A
    children#2 :: [A x A] -> A
    children#3 :: [A x A x A x A] -> A
    copyover :: [A x A] -> A
    copyover#1 :: [A] -> A
    copyover#2 :: [A x A] -> A
    dequeue :: [A x A] -> A
    dequeue#1 :: [A] -> A
    dequeue#2 :: [A x A] -> A
    dequeue#3 :: [A] -> A
    dequeue#4 :: [A] -> A
    empty :: [A] -> A
    enqueue :: [A x A] -> A
    enqueue#1 :: [A x A] -> A
    enqueues :: [A x A] -> A
    enqueues#1 :: [A x A] -> A
    startBreadth :: [A] -> A
    startBreadth#1 :: [A] -> A
    startBreadth#2 :: [A] -> A)
(RULES
    breadth(@breadth@1
           ,@breadth@2) ->
      breadth#1(dequeue(@breadth@1
                       ,@breadth@2))
    breadth#1(tuple#2(@queue'
                     ,@elem)) -> breadth#2(@elem
                                          ,@queue')
    breadth#2(::(@z,@_@9)
             ,@queue') ->
      breadth#3(breadth#4(@z),@queue')
    breadth#2(nil(),@queue') ->
      nil()
    breadth#3(tuple#2(@x,@ys)
             ,@queue') -> ::(@x
                            ,breadth#5(enqueues(@ys
                                               ,@queue')))
    breadth#4(tuple#4(@children@3
                     ,@children@4
                     ,@children@5
                     ,@children@6)) ->
      children(@children@3
              ,@children@4
              ,@children@5
              ,@children@6)
    breadth#5(tuple#2(@breadth@7
                     ,@breadth@8)) ->
      breadth(@breadth@7,@breadth@8)
    children(@a,@b,@l1,@l2) ->
      tuple#2(tuple#2(@a,@b)
             ,children#1(@l1,@b,@l2))
    children#1(::(@x,@xs),@b,@l2) ->
      children#3(@l2,@b,@x,@xs)
    children#1(nil(),@b,@l2) ->
      children#2(@l2,@b)
    children#2(::(@y,@ys),@b) ->
      ::(tuple#4(@y,@b,nil(),@ys)
        ,nil())
    children#2(nil(),@b) -> nil()
    children#3(::(@y,@ys)
              ,@b
              ,@x
              ,@xs) -> ::(tuple#4(@x
                                 ,@b
                                 ,nil()
                                 ,@xs)
                         ,::(tuple#4(@x,@y,@xs,@ys)
                            ,nil()))
    children#3(nil(),@b,@x,@xs) ->
      nil()
    copyover(@copyover@1
            ,@copyover@2) ->
      copyover#1(tuple#2(@copyover@1
                        ,@copyover@2))
    copyover#1(tuple#2(@inq
                      ,@outq)) -> copyover#2(@inq
                                            ,@outq)
    copyover#2(::(@x,@xs),@outq) ->
      copyover(@xs,::(@x,@outq))
    copyover#2(nil(),@outq) ->
      tuple#2(nil(),@outq)
    dequeue(@dequeue@1
           ,@dequeue@2) ->
      dequeue#1(tuple#2(@dequeue@1
                       ,@dequeue@2))
    dequeue#1(tuple#2(@inq
                     ,@outq)) -> dequeue#2(@outq
                                          ,@inq)
    dequeue#2(::(@y,@ys),@inq) ->
      tuple#2(tuple#2(@inq,@ys)
             ,::(@y,nil()))
    dequeue#2(nil(),@inq) ->
      dequeue#3(@inq)
    dequeue#3(::(@x,@xs)) ->
      dequeue#4(copyover(::(@x,@xs)
                        ,nil()))
    dequeue#3(nil()) ->
      tuple#2(tuple#2(nil(),nil())
             ,nil())
    dequeue#4(tuple#2(@dequeue@3
                     ,@dequeue@4)) ->
      dequeue(@dequeue@3,@dequeue@4)
    empty(@x) -> tuple#2(nil()
                        ,nil())
    enqueue(@x,@queue) ->
      enqueue#1(@queue,@x)
    enqueue#1(tuple#2(@inq,@outq)
             ,@x) -> tuple#2(::(@x,@inq)
                            ,@outq)
    enqueues(@l,@queue) ->
      enqueues#1(@l,@queue)
    enqueues#1(::(@x,@xs),@queue) ->
      enqueues(@xs,enqueue(@x,@queue))
    enqueues#1(nil(),@queue) ->
      @queue
    startBreadth(@xs) ->
      startBreadth#1(@xs)
    startBreadth#1(::(@x,@xs)) ->
      startBreadth#2(enqueue(tuple#4(@x
                                    ,@x
                                    ,@xs
                                    ,@xs)
                            ,empty(#unit())))
    startBreadth#1(nil()) -> nil()
    startBreadth#2(tuple#2(@breadth@1
                          ,@breadth@2)) ->
      breadth(@breadth@1,@breadth@2))