Runtime Complexity TRS:
The TRS R consists of the following 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)

Rewrite Strategy: INNERMOST


Renamed function symbols to avoid clashes with predefined symbol.


Runtime Complexity TRS:
The TRS R consists of the following 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)

Rewrite Strategy: INNERMOST


Sliced the following arguments:
empty'/0


Runtime Complexity TRS:
The TRS R consists of the following 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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Rewrite Strategy: INNERMOST


Infered types.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'


Heuristically decided to analyse the following defined symbols:
breadth#1', dequeue', breadth#5', enqueues', copyover', copyover#1', dequeue#1', dequeue#3', dequeue#4', enqueues#1'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'
enqueues' < breadth#1'
dequeue' < breadth#5'
dequeue' = dequeue#1'
dequeue' = dequeue#3'
dequeue' = dequeue#4'
enqueues' = enqueues#1'
copyover' = copyover#1'
copyover' < dequeue#3'
dequeue#1' = dequeue#3'
dequeue#1' = dequeue#4'
dequeue#3' = dequeue#4'


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
copyover#1', breadth#1', dequeue', breadth#5', enqueues', copyover', dequeue#1', dequeue#3', dequeue#4', enqueues#1'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'
enqueues' < breadth#1'
dequeue' < breadth#5'
dequeue' = dequeue#1'
dequeue' = dequeue#3'
dequeue' = dequeue#4'
enqueues' = enqueues#1'
copyover' = copyover#1'
copyover' < dequeue#3'
dequeue#1' = dequeue#3'
dequeue#1' = dequeue#4'
dequeue#3' = dequeue#4'


Could not prove a rewrite lemma for the defined symbol copyover#1'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
copyover', breadth#1', dequeue', breadth#5', enqueues', dequeue#1', dequeue#3', dequeue#4', enqueues#1'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'
enqueues' < breadth#1'
dequeue' < breadth#5'
dequeue' = dequeue#1'
dequeue' = dequeue#3'
dequeue' = dequeue#4'
enqueues' = enqueues#1'
copyover' = copyover#1'
copyover' < dequeue#3'
dequeue#1' = dequeue#3'
dequeue#1' = dequeue#4'
dequeue#3' = dequeue#4'


Could not prove a rewrite lemma for the defined symbol copyover'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
enqueues#1', breadth#1', dequeue', breadth#5', enqueues', dequeue#1', dequeue#3', dequeue#4'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'
enqueues' < breadth#1'
dequeue' < breadth#5'
dequeue' = dequeue#1'
dequeue' = dequeue#3'
dequeue' = dequeue#4'
enqueues' = enqueues#1'
dequeue#1' = dequeue#3'
dequeue#1' = dequeue#4'
dequeue#3' = dequeue#4'


Could not prove a rewrite lemma for the defined symbol enqueues#1'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
enqueues', breadth#1', dequeue', breadth#5', dequeue#1', dequeue#3', dequeue#4'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'
enqueues' < breadth#1'
dequeue' < breadth#5'
dequeue' = dequeue#1'
dequeue' = dequeue#3'
dequeue' = dequeue#4'
enqueues' = enqueues#1'
dequeue#1' = dequeue#3'
dequeue#1' = dequeue#4'
dequeue#3' = dequeue#4'


Could not prove a rewrite lemma for the defined symbol enqueues'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
dequeue#1', breadth#1', dequeue', breadth#5', dequeue#3', dequeue#4'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'
dequeue' < breadth#5'
dequeue' = dequeue#1'
dequeue' = dequeue#3'
dequeue' = dequeue#4'
dequeue#1' = dequeue#3'
dequeue#1' = dequeue#4'
dequeue#3' = dequeue#4'


Could not prove a rewrite lemma for the defined symbol dequeue#1'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
dequeue#3', breadth#1', dequeue', breadth#5', dequeue#4'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'
dequeue' < breadth#5'
dequeue' = dequeue#1'
dequeue' = dequeue#3'
dequeue' = dequeue#4'
dequeue#1' = dequeue#3'
dequeue#1' = dequeue#4'
dequeue#3' = dequeue#4'


Could not prove a rewrite lemma for the defined symbol dequeue#3'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
dequeue#4', breadth#1', dequeue', breadth#5'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'
dequeue' < breadth#5'
dequeue' = dequeue#1'
dequeue' = dequeue#3'
dequeue' = dequeue#4'
dequeue#1' = dequeue#3'
dequeue#1' = dequeue#4'
dequeue#3' = dequeue#4'


Could not prove a rewrite lemma for the defined symbol dequeue#4'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
dequeue', breadth#1', breadth#5'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'
dequeue' < breadth#5'
dequeue' = dequeue#1'
dequeue' = dequeue#3'
dequeue' = dequeue#4'
dequeue#1' = dequeue#3'
dequeue#1' = dequeue#4'
dequeue#3' = dequeue#4'


Could not prove a rewrite lemma for the defined symbol dequeue'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
breadth#5', breadth#1'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'


Could not prove a rewrite lemma for the defined symbol breadth#5'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

The following defined symbols remain to be analysed:
breadth#1'

They will be analysed ascendingly in the following order:
breadth#1' = breadth#5'


Could not prove a rewrite lemma for the defined symbol breadth#1'.


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'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'))
startBreadth#1'(nil') → nil'
startBreadth#2'(tuple#2'(@breadth@1, @breadth@2)) → breadth'(@breadth@1, @breadth@2)

Types:
breadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
::' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
breadth#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
nil' :: tuple#2':::':nil':tuple#4'
breadth#5' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
tuple#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
children#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
copyover#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#3' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
dequeue#4' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
empty' :: tuple#2':::':nil':tuple#4'
enqueue' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueue#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
enqueues#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#1' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
startBreadth#2' :: tuple#2':::':nil':tuple#4' → tuple#2':::':nil':tuple#4'
_hole_tuple#2':::':nil':tuple#4'1 :: tuple#2':::':nil':tuple#4'
_gen_tuple#2':::':nil':tuple#4'2 :: Nat → tuple#2':::':nil':tuple#4'

Generator Equations:
_gen_tuple#2':::':nil':tuple#4'2(0) ⇔ nil'
_gen_tuple#2':::':nil':tuple#4'2(+(x, 1)) ⇔ tuple#2'(nil', _gen_tuple#2':::':nil':tuple#4'2(x))

No more defined symbols left to analyse.