The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(n^1, INF).

(0) Obligation:

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

(1) DecreasingLoopProof (EQUIVALENT transformation)

The following loop(s) give(s) rise to the lower bound Ω(n¹):
The rewrite sequence
breadth(@breadth@1, ::(tuple#4(@children@31760_0, @children@41761_0, ::(@x3138_0, @xs3139_0), nil), @ys281_0)) →⁺ ::(tuple#2(@children@31760_0, @children@41761_0), breadth(@breadth@1, @ys281_0))
gives rise to a decreasing loop by considering the right hand sides subterm at position [1].
The pumping substitution is [@ys281_0 / ::(tuple#4(@children@31760_0, @children@41761_0, ::(@x3138_0, @xs3139_0), nil), @ys281_0)].
The result substitution is [ ].

(2) BOUNDS(n^1, INF)

(3) RenamingProof (EQUIVALENT transformation)

Renamed function symbols to avoid clashes with predefined symbol.

(4) Obligation:

Runtime Complexity Relative 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)

S is empty.
Rewrite Strategy: INNERMOST

(5) SlicingProof (LOWER BOUND(ID) transformation)

Sliced the following arguments:
empty/0

(6) Obligation:

Runtime Complexity Relative 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)

S is empty.
Rewrite Strategy: INNERMOST

(7) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(8) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

(9) OrderProof (LOWER BOUND(ID) transformation)

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

(10) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(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

(11) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(12) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(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

(13) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(14) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(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

(15) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(16) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(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

(17) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(18) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(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

(19) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(20) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(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

(21) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(22) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(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

(23) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(24) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(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

(25) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(26) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(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

(27) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(28) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(x))

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

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

(29) NoRewriteLemmaProof (LOWER BOUND(ID) transformation)

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

(30) Obligation:

Innermost TRS:
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#41_0 :: tuple#2::::nil:tuple#4
gen_tuple#2::::nil:tuple#42_0 :: Nat → tuple#2::::nil:tuple#4

Generator Equations:
gen_tuple#2::::nil:tuple#42_0(0) ⇔ nil
gen_tuple#2::::nil:tuple#42_0(+(x, 1)) ⇔ tuple#2(nil, gen_tuple#2::::nil:tuple#42_0(x))

No more defined symbols left to analyse.