MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { breadth(@breadth@1, @breadth@2) -> breadth#1(dequeue(@breadth@1, @breadth@2)) , dequeue(@dequeue@1, @dequeue@2) -> dequeue#1(tuple#2(@dequeue@1, @dequeue@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#4(tuple#4(@children@3, @children@4, @children@5, @children@6)) -> children(@children@3, @children@4, @children@5, @children@6) , breadth#3(tuple#2(@x, @ys), @queue') -> ::(@x, breadth#5(enqueues(@ys, @queue'))) , enqueues(@l, @queue) -> enqueues#1(@l, @queue) , 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#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() , children#2(::(@y, @ys), @b) -> ::(tuple#4(@y, @b, nil(), @ys), nil()) , children#2(nil(), @b) -> 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#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#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) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { breadth#2(nil(), @queue') -> nil() , startBreadth#1(nil()) -> nil() , startBreadth#2(tuple#2(@breadth@1, @breadth@2)) -> breadth(@breadth@1, @breadth@2) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(breadth#1) = {1}, Uargs(tuple#2) = {2}, Uargs(::) = {2}, Uargs(breadth#3) = {1}, Uargs(enqueues) = {2}, Uargs(breadth#5) = {1}, Uargs(dequeue#4) = {1}, Uargs(enqueue) = {2}, Uargs(startBreadth#2) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [breadth](x1, x2) = [2 2] x2 + [1] [0 0] [0] [dequeue](x1, x2) = [0 0] x2 + [0] [1 1] [0] [breadth#1](x1) = [1 2] x1 + [1] [0 0] [0] [tuple#2](x1, x2) = [0 0] x1 + [1 1] x2 + [0] [1 0] [0 0] [0] [breadth#2](x1, x2) = [2 0] x2 + [1] [0 0] [0] [::](x1, x2) = [1 0] x2 + [0] [0 1] [0] [breadth#4](x1) = [0 0] x1 + [0] [0 1] [0] [breadth#3](x1, x2) = [2 0] x1 + [2 0] x2 + [1] [0 0] [0 0] [0] [nil] = [0] [0] [enqueues](x1, x2) = [1 0] x2 + [0] [0 1] [0] [breadth#5](x1) = [2 0] x1 + [1] [0 0] [0] [tuple#4](x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [1 0] x3 + [0 0] x4 + [0] [1 1] [1 1] [0 0] [1 1] [0] [children](x1, x2, x3, x4) = [0 0] x2 + [0] [1 1] [0] [children#1](x1, x2, x3) = [0] [0] [children#3](x1, x2, x3, x4) = [0] [0] [children#2](x1, x2) = [0] [0] [copyover](x1, x2) = [1 1] x2 + [0] [0 0] [0] [copyover#1](x1) = [1 0] x1 + [0] [0 0] [0] [copyover#2](x1, x2) = [1 1] x2 + [0] [0 0] [0] [dequeue#1](x1) = [0 0] x1 + [0] [1 0] [0] [dequeue#2](x1, x2) = [0 0] x1 + [0] [1 1] [0] [dequeue#3](x1) = [0] [0] [dequeue#4](x1) = [1 2] x1 + [0] [1 0] [0] [empty](x1) = [0] [0] [enqueue](x1, x2) = [1 0] x2 + [0] [0 1] [0] [enqueue#1](x1, x2) = [1 0] x1 + [0] [0 1] [0] [enqueues#1](x1, x2) = [1 0] x2 + [0] [0 1] [0] [startBreadth](x1) = [2 2] x1 + [2] [2 2] [2] [startBreadth#1](x1) = [2] [0] [#unit] = [0] [0] [startBreadth#2](x1) = [2 0] x1 + [2] [0 0] [0] This order satisfies following ordering constraints [breadth(@breadth@1, @breadth@2)] = [2 2] @breadth@2 + [1] [0 0] [0] >= [2 2] @breadth@2 + [1] [0 0] [0] = [breadth#1(dequeue(@breadth@1, @breadth@2))] [dequeue(@dequeue@1, @dequeue@2)] = [0 0] @dequeue@2 + [0] [1 1] [0] >= [0 0] @dequeue@2 + [0] [1 1] [0] = [dequeue#1(tuple#2(@dequeue@1, @dequeue@2))] [breadth#1(tuple#2(@queue', @elem))] = [1 1] @elem + [2 0] @queue' + [1] [0 0] [0 0] [0] >= [2 0] @queue' + [1] [0 0] [0] = [breadth#2(@elem, @queue')] [breadth#2(::(@z, @_@9), @queue')] = [2 0] @queue' + [1] [0 0] [0] >= [2 0] @queue' + [1] [0 0] [0] = [breadth#3(breadth#4(@z), @queue')] [breadth#2(nil(), @queue')] = [2 0] @queue' + [1] [0 0] [0] > [0] [0] = [nil()] [breadth#4(tuple#4(@children@3, = [0 0] @children@3 + [0 0] @children@4 + [0 0] @children@6 + [0] @children@4, [1 1] [1 1] [1 1] [0] @children@5, @children@6))] >= [0 0] @children@4 + [0] [1 1] [0] = [children(@children@3, @children@4, @children@5, @children@6)] [breadth#3(tuple#2(@x, @ys), @queue')] = [2 0] @queue' + [2 2] @ys + [1] [0 0] [0 0] [0] >= [2 0] @queue' + [1] [0 0] [0] = [::(@x, breadth#5(enqueues(@ys, @queue')))] [enqueues(@l, @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueues#1(@l, @queue)] [breadth#5(tuple#2(@breadth@7, @breadth@8))] = [2 2] @breadth@8 + [1] [0 0] [0] >= [2 2] @breadth@8 + [1] [0 0] [0] = [breadth(@breadth@7, @breadth@8)] [children(@a, @b, @l1, @l2)] = [0 0] @b + [0] [1 1] [0] >= [0 0] @b + [0] [1 1] [0] = [tuple#2(tuple#2(@a, @b), children#1(@l1, @b, @l2))] [children#1(::(@x, @xs), @b, @l2)] = [0] [0] >= [0] [0] = [children#3(@l2, @b, @x, @xs)] [children#1(nil(), @b, @l2)] = [0] [0] >= [0] [0] = [children#2(@l2, @b)] [children#3(::(@y, @ys), @b, @x, @xs)] = [0] [0] >= [0] [0] = [::(tuple#4(@x, @b, nil(), @xs), ::(tuple#4(@x, @y, @xs, @ys), nil()))] [children#3(nil(), @b, @x, @xs)] = [0] [0] >= [0] [0] = [nil()] [children#2(::(@y, @ys), @b)] = [0] [0] >= [0] [0] = [::(tuple#4(@y, @b, nil(), @ys), nil())] [children#2(nil(), @b)] = [0] [0] >= [0] [0] = [nil()] [copyover(@copyover@1, @copyover@2)] = [1 1] @copyover@2 + [0] [0 0] [0] >= [1 1] @copyover@2 + [0] [0 0] [0] = [copyover#1(tuple#2(@copyover@1, @copyover@2))] [copyover#1(tuple#2(@inq, @outq))] = [1 1] @outq + [0] [0 0] [0] >= [1 1] @outq + [0] [0 0] [0] = [copyover#2(@inq, @outq)] [copyover#2(::(@x, @xs), @outq)] = [1 1] @outq + [0] [0 0] [0] >= [1 1] @outq + [0] [0 0] [0] = [copyover(@xs, ::(@x, @outq))] [copyover#2(nil(), @outq)] = [1 1] @outq + [0] [0 0] [0] >= [1 1] @outq + [0] [0 0] [0] = [tuple#2(nil(), @outq)] [dequeue#1(tuple#2(@inq, @outq))] = [0 0] @outq + [0] [1 1] [0] >= [0 0] @outq + [0] [1 1] [0] = [dequeue#2(@outq, @inq)] [dequeue#2(::(@y, @ys), @inq)] = [0 0] @ys + [0] [1 1] [0] >= [0 0] @ys + [0] [1 1] [0] = [tuple#2(tuple#2(@inq, @ys), ::(@y, nil()))] [dequeue#2(nil(), @inq)] = [0] [0] >= [0] [0] = [dequeue#3(@inq)] [dequeue#3(::(@x, @xs))] = [0] [0] >= [0] [0] = [dequeue#4(copyover(::(@x, @xs), nil()))] [dequeue#3(nil())] = [0] [0] >= [0] [0] = [tuple#2(tuple#2(nil(), nil()), nil())] [dequeue#4(tuple#2(@dequeue@3, @dequeue@4))] = [2 0] @dequeue@3 + [1 1] @dequeue@4 + [0] [0 0] [1 1] [0] >= [0 0] @dequeue@4 + [0] [1 1] [0] = [dequeue(@dequeue@3, @dequeue@4)] [empty(@x)] = [0] [0] >= [0] [0] = [tuple#2(nil(), nil())] [enqueue(@x, @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueue#1(@queue, @x)] [enqueue#1(tuple#2(@inq, @outq), @x)] = [0 0] @inq + [1 1] @outq + [0] [1 0] [0 0] [0] >= [0 0] @inq + [1 1] @outq + [0] [1 0] [0 0] [0] = [tuple#2(::(@x, @inq), @outq)] [enqueues#1(::(@x, @xs), @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueues(@xs, enqueue(@x, @queue))] [enqueues#1(nil(), @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [@queue] [startBreadth(@xs)] = [2 2] @xs + [2] [2 2] [2] >= [2] [0] = [startBreadth#1(@xs)] [startBreadth#1(::(@x, @xs))] = [2] [0] >= [2] [0] = [startBreadth#2(enqueue(tuple#4(@x, @x, @xs, @xs), empty(#unit())))] [startBreadth#1(nil())] = [2] [0] > [0] [0] = [nil()] [startBreadth#2(tuple#2(@breadth@1, @breadth@2))] = [2 2] @breadth@2 + [2] [0 0] [0] > [2 2] @breadth@2 + [1] [0 0] [0] = [breadth(@breadth@1, @breadth@2)] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { breadth(@breadth@1, @breadth@2) -> breadth#1(dequeue(@breadth@1, @breadth@2)) , dequeue(@dequeue@1, @dequeue@2) -> dequeue#1(tuple#2(@dequeue@1, @dequeue@2)) , breadth#1(tuple#2(@queue', @elem)) -> breadth#2(@elem, @queue') , breadth#2(::(@z, @_@9), @queue') -> breadth#3(breadth#4(@z), @queue') , breadth#4(tuple#4(@children@3, @children@4, @children@5, @children@6)) -> children(@children@3, @children@4, @children@5, @children@6) , breadth#3(tuple#2(@x, @ys), @queue') -> ::(@x, breadth#5(enqueues(@ys, @queue'))) , enqueues(@l, @queue) -> enqueues#1(@l, @queue) , 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#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() , children#2(::(@y, @ys), @b) -> ::(tuple#4(@y, @b, nil(), @ys), nil()) , children#2(nil(), @b) -> 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#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#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()))) } Weak Trs: { breadth#2(nil(), @queue') -> nil() , startBreadth#1(nil()) -> nil() , startBreadth#2(tuple#2(@breadth@1, @breadth@2)) -> breadth(@breadth@1, @breadth@2) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { empty(@x) -> tuple#2(nil(), nil()) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(breadth#1) = {1}, Uargs(tuple#2) = {2}, Uargs(::) = {2}, Uargs(breadth#3) = {1}, Uargs(enqueues) = {2}, Uargs(breadth#5) = {1}, Uargs(dequeue#4) = {1}, Uargs(enqueue) = {2}, Uargs(startBreadth#2) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [breadth](x1, x2) = [1 1] x1 + [1 0] x2 + [1] [0 0] [0 0] [0] [dequeue](x1, x2) = [0 0] x1 + [0 0] x2 + [0] [1 1] [1 0] [0] [breadth#1](x1) = [2 1] x1 + [1] [0 0] [0] [tuple#2](x1, x2) = [0 0] x1 + [1 0] x2 + [0] [1 1] [0 0] [0] [breadth#2](x1, x2) = [1 0] x1 + [1 1] x2 + [1] [0 0] [0 0] [0] [::](x1, x2) = [1 0] x2 + [0] [0 0] [0] [breadth#4](x1) = [0 0] x1 + [0] [2 0] [0] [breadth#3](x1, x2) = [1 0] x1 + [1 1] x2 + [1] [0 0] [0 0] [0] [nil] = [0] [0] [enqueues](x1, x2) = [1 0] x2 + [0] [0 1] [0] [breadth#5](x1) = [1 1] x1 + [1] [0 0] [0] [tuple#4](x1, x2, x3, x4) = [1 1] x1 + [1 0] x2 + [0 0] x3 + [1 0] x4 + [0] [0 0] [0 1] [1 1] [0 1] [2] [children](x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0] [2 2] [2 0] [0] [children#1](x1, x2, x3) = [0] [0] [children#3](x1, x2, x3, x4) = [0] [0] [children#2](x1, x2) = [0] [0] [copyover](x1, x2) = [2 0] x2 + [0] [0 0] [0] [copyover#1](x1) = [2 0] x1 + [0] [0 0] [0] [copyover#2](x1, x2) = [2 0] x2 + [0] [0 0] [0] [dequeue#1](x1) = [0 0] x1 + [0] [1 1] [0] [dequeue#2](x1, x2) = [0 0] x1 + [0 0] x2 + [0] [1 0] [1 1] [0] [dequeue#3](x1) = [0] [0] [dequeue#4](x1) = [2 0] x1 + [0] [2 1] [0] [empty](x1) = [1] [0] [enqueue](x1, x2) = [1 0] x2 + [0] [0 1] [0] [enqueue#1](x1, x2) = [1 0] x1 + [0] [0 1] [0] [enqueues#1](x1, x2) = [1 0] x2 + [0] [0 1] [0] [startBreadth](x1) = [2 2] x1 + [2] [2 2] [2] [startBreadth#1](x1) = [0 0] x1 + [2] [1 1] [0] [#unit] = [0] [0] [startBreadth#2](x1) = [1 2] x1 + [1] [0 0] [0] This order satisfies following ordering constraints [breadth(@breadth@1, @breadth@2)] = [1 1] @breadth@1 + [1 0] @breadth@2 + [1] [0 0] [0 0] [0] >= [1 1] @breadth@1 + [1 0] @breadth@2 + [1] [0 0] [0 0] [0] = [breadth#1(dequeue(@breadth@1, @breadth@2))] [dequeue(@dequeue@1, @dequeue@2)] = [0 0] @dequeue@1 + [0 0] @dequeue@2 + [0] [1 1] [1 0] [0] >= [0 0] @dequeue@1 + [0 0] @dequeue@2 + [0] [1 1] [1 0] [0] = [dequeue#1(tuple#2(@dequeue@1, @dequeue@2))] [breadth#1(tuple#2(@queue', @elem))] = [2 0] @elem + [1 1] @queue' + [1] [0 0] [0 0] [0] >= [1 0] @elem + [1 1] @queue' + [1] [0 0] [0 0] [0] = [breadth#2(@elem, @queue')] [breadth#2(::(@z, @_@9), @queue')] = [1 0] @_@9 + [1 1] @queue' + [1] [0 0] [0 0] [0] >= [1 1] @queue' + [1] [0 0] [0] = [breadth#3(breadth#4(@z), @queue')] [breadth#2(nil(), @queue')] = [1 1] @queue' + [1] [0 0] [0] > [0] [0] = [nil()] [breadth#4(tuple#4(@children@3, = [0 0] @children@3 + [0 0] @children@4 + [0 0] @children@6 + [0] @children@4, [2 2] [2 0] [2 0] [0] @children@5, @children@6))] >= [0 0] @children@3 + [0 0] @children@4 + [0] [2 2] [2 0] [0] = [children(@children@3, @children@4, @children@5, @children@6)] [breadth#3(tuple#2(@x, @ys), @queue')] = [1 1] @queue' + [1 0] @ys + [1] [0 0] [0 0] [0] >= [1 1] @queue' + [1] [0 0] [0] = [::(@x, breadth#5(enqueues(@ys, @queue')))] [enqueues(@l, @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueues#1(@l, @queue)] [breadth#5(tuple#2(@breadth@7, @breadth@8))] = [1 1] @breadth@7 + [1 0] @breadth@8 + [1] [0 0] [0 0] [0] >= [1 1] @breadth@7 + [1 0] @breadth@8 + [1] [0 0] [0 0] [0] = [breadth(@breadth@7, @breadth@8)] [children(@a, @b, @l1, @l2)] = [0 0] @a + [0 0] @b + [0] [2 2] [2 0] [0] >= [0 0] @a + [0 0] @b + [0] [1 1] [1 0] [0] = [tuple#2(tuple#2(@a, @b), children#1(@l1, @b, @l2))] [children#1(::(@x, @xs), @b, @l2)] = [0] [0] >= [0] [0] = [children#3(@l2, @b, @x, @xs)] [children#1(nil(), @b, @l2)] = [0] [0] >= [0] [0] = [children#2(@l2, @b)] [children#3(::(@y, @ys), @b, @x, @xs)] = [0] [0] >= [0] [0] = [::(tuple#4(@x, @b, nil(), @xs), ::(tuple#4(@x, @y, @xs, @ys), nil()))] [children#3(nil(), @b, @x, @xs)] = [0] [0] >= [0] [0] = [nil()] [children#2(::(@y, @ys), @b)] = [0] [0] >= [0] [0] = [::(tuple#4(@y, @b, nil(), @ys), nil())] [children#2(nil(), @b)] = [0] [0] >= [0] [0] = [nil()] [copyover(@copyover@1, @copyover@2)] = [2 0] @copyover@2 + [0] [0 0] [0] >= [2 0] @copyover@2 + [0] [0 0] [0] = [copyover#1(tuple#2(@copyover@1, @copyover@2))] [copyover#1(tuple#2(@inq, @outq))] = [2 0] @outq + [0] [0 0] [0] >= [2 0] @outq + [0] [0 0] [0] = [copyover#2(@inq, @outq)] [copyover#2(::(@x, @xs), @outq)] = [2 0] @outq + [0] [0 0] [0] >= [2 0] @outq + [0] [0 0] [0] = [copyover(@xs, ::(@x, @outq))] [copyover#2(nil(), @outq)] = [2 0] @outq + [0] [0 0] [0] >= [1 0] @outq + [0] [0 0] [0] = [tuple#2(nil(), @outq)] [dequeue#1(tuple#2(@inq, @outq))] = [0 0] @inq + [0 0] @outq + [0] [1 1] [1 0] [0] >= [0 0] @inq + [0 0] @outq + [0] [1 1] [1 0] [0] = [dequeue#2(@outq, @inq)] [dequeue#2(::(@y, @ys), @inq)] = [0 0] @inq + [0 0] @ys + [0] [1 1] [1 0] [0] >= [0 0] @inq + [0 0] @ys + [0] [1 1] [1 0] [0] = [tuple#2(tuple#2(@inq, @ys), ::(@y, nil()))] [dequeue#2(nil(), @inq)] = [0 0] @inq + [0] [1 1] [0] >= [0] [0] = [dequeue#3(@inq)] [dequeue#3(::(@x, @xs))] = [0] [0] >= [0] [0] = [dequeue#4(copyover(::(@x, @xs), nil()))] [dequeue#3(nil())] = [0] [0] >= [0] [0] = [tuple#2(tuple#2(nil(), nil()), nil())] [dequeue#4(tuple#2(@dequeue@3, @dequeue@4))] = [0 0] @dequeue@3 + [2 0] @dequeue@4 + [0] [1 1] [2 0] [0] >= [0 0] @dequeue@3 + [0 0] @dequeue@4 + [0] [1 1] [1 0] [0] = [dequeue(@dequeue@3, @dequeue@4)] [empty(@x)] = [1] [0] > [0] [0] = [tuple#2(nil(), nil())] [enqueue(@x, @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueue#1(@queue, @x)] [enqueue#1(tuple#2(@inq, @outq), @x)] = [0 0] @inq + [1 0] @outq + [0] [1 1] [0 0] [0] >= [0 0] @inq + [1 0] @outq + [0] [1 0] [0 0] [0] = [tuple#2(::(@x, @inq), @outq)] [enqueues#1(::(@x, @xs), @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueues(@xs, enqueue(@x, @queue))] [enqueues#1(nil(), @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [@queue] [startBreadth(@xs)] = [2 2] @xs + [2] [2 2] [2] >= [0 0] @xs + [2] [1 1] [0] = [startBreadth#1(@xs)] [startBreadth#1(::(@x, @xs))] = [0 0] @xs + [2] [1 0] [0] >= [2] [0] = [startBreadth#2(enqueue(tuple#4(@x, @x, @xs, @xs), empty(#unit())))] [startBreadth#1(nil())] = [2] [0] > [0] [0] = [nil()] [startBreadth#2(tuple#2(@breadth@1, @breadth@2))] = [2 2] @breadth@1 + [1 0] @breadth@2 + [1] [0 0] [0 0] [0] >= [1 1] @breadth@1 + [1 0] @breadth@2 + [1] [0 0] [0 0] [0] = [breadth(@breadth@1, @breadth@2)] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { breadth(@breadth@1, @breadth@2) -> breadth#1(dequeue(@breadth@1, @breadth@2)) , dequeue(@dequeue@1, @dequeue@2) -> dequeue#1(tuple#2(@dequeue@1, @dequeue@2)) , breadth#1(tuple#2(@queue', @elem)) -> breadth#2(@elem, @queue') , breadth#2(::(@z, @_@9), @queue') -> breadth#3(breadth#4(@z), @queue') , breadth#4(tuple#4(@children@3, @children@4, @children@5, @children@6)) -> children(@children@3, @children@4, @children@5, @children@6) , breadth#3(tuple#2(@x, @ys), @queue') -> ::(@x, breadth#5(enqueues(@ys, @queue'))) , enqueues(@l, @queue) -> enqueues#1(@l, @queue) , 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#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() , children#2(::(@y, @ys), @b) -> ::(tuple#4(@y, @b, nil(), @ys), nil()) , children#2(nil(), @b) -> 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#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) , enqueue(@x, @queue) -> enqueue#1(@queue, @x) , enqueue#1(tuple#2(@inq, @outq), @x) -> tuple#2(::(@x, @inq), @outq) , 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()))) } Weak Trs: { breadth#2(nil(), @queue') -> nil() , empty(@x) -> tuple#2(nil(), nil()) , startBreadth#1(nil()) -> nil() , startBreadth#2(tuple#2(@breadth@1, @breadth@2)) -> breadth(@breadth@1, @breadth@2) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { startBreadth#1(::(@x, @xs)) -> startBreadth#2(enqueue(tuple#4(@x, @x, @xs, @xs), empty(#unit()))) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(breadth#1) = {1}, Uargs(tuple#2) = {2}, Uargs(::) = {2}, Uargs(breadth#3) = {1}, Uargs(enqueues) = {2}, Uargs(breadth#5) = {1}, Uargs(dequeue#4) = {1}, Uargs(enqueue) = {2}, Uargs(startBreadth#2) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [breadth](x1, x2) = [1 1] x1 + [2 0] x2 + [0] [0 0] [0 0] [2] [dequeue](x1, x2) = [0 0] x1 + [0 0] x2 + [0] [1 1] [2 0] [0] [breadth#1](x1) = [1 1] x1 + [0] [0 0] [2] [tuple#2](x1, x2) = [0 0] x1 + [1 0] x2 + [0] [1 1] [1 0] [0] [breadth#2](x1, x2) = [1 1] x2 + [0] [0 0] [0] [::](x1, x2) = [1 0] x2 + [0] [0 0] [0] [breadth#4](x1) = [0 0] x1 + [0] [1 1] [2] [breadth#3](x1, x2) = [1 0] x1 + [1 1] x2 + [0] [0 0] [0 0] [0] [nil] = [0] [0] [enqueues](x1, x2) = [1 0] x2 + [0] [0 1] [0] [breadth#5](x1) = [1 1] x1 + [0] [0 0] [2] [tuple#4](x1, x2, x3, x4) = [0 0] x1 + [1 0] x2 + [0 0] x4 + [0] [1 1] [1 0] [1 1] [0] [children](x1, x2, x3, x4) = [0 0] x1 + [0 0] x2 + [0] [1 1] [2 0] [0] [children#1](x1, x2, x3) = [0 0] x2 + [0] [1 0] [0] [children#3](x1, x2, x3, x4) = [0] [0] [children#2](x1, x2) = [0] [0] [copyover](x1, x2) = [2 1] x2 + [0] [2 0] [0] [copyover#1](x1) = [2 0] x1 + [0] [2 0] [0] [copyover#2](x1, x2) = [2 0] x2 + [0] [2 0] [0] [dequeue#1](x1) = [0 0] x1 + [0] [1 1] [0] [dequeue#2](x1, x2) = [0 0] x1 + [0 0] x2 + [0] [2 0] [1 1] [0] [dequeue#3](x1) = [0] [0] [dequeue#4](x1) = [1 1] x1 + [0] [1 2] [0] [empty](x1) = [0] [0] [enqueue](x1, x2) = [1 0] x2 + [0] [0 1] [0] [enqueue#1](x1, x2) = [1 0] x1 + [0] [0 1] [0] [enqueues#1](x1, x2) = [1 0] x2 + [0] [0 1] [0] [startBreadth](x1) = [2 2] x1 + [2] [2 2] [2] [startBreadth#1](x1) = [2 2] x1 + [2] [2 0] [2] [#unit] = [0] [0] [startBreadth#2](x1) = [2 2] x1 + [0] [2 0] [2] This order satisfies following ordering constraints [breadth(@breadth@1, @breadth@2)] = [1 1] @breadth@1 + [2 0] @breadth@2 + [0] [0 0] [0 0] [2] >= [1 1] @breadth@1 + [2 0] @breadth@2 + [0] [0 0] [0 0] [2] = [breadth#1(dequeue(@breadth@1, @breadth@2))] [dequeue(@dequeue@1, @dequeue@2)] = [0 0] @dequeue@1 + [0 0] @dequeue@2 + [0] [1 1] [2 0] [0] >= [0 0] @dequeue@1 + [0 0] @dequeue@2 + [0] [1 1] [2 0] [0] = [dequeue#1(tuple#2(@dequeue@1, @dequeue@2))] [breadth#1(tuple#2(@queue', @elem))] = [2 0] @elem + [1 1] @queue' + [0] [0 0] [0 0] [2] >= [1 1] @queue' + [0] [0 0] [0] = [breadth#2(@elem, @queue')] [breadth#2(::(@z, @_@9), @queue')] = [1 1] @queue' + [0] [0 0] [0] >= [1 1] @queue' + [0] [0 0] [0] = [breadth#3(breadth#4(@z), @queue')] [breadth#2(nil(), @queue')] = [1 1] @queue' + [0] [0 0] [0] >= [0] [0] = [nil()] [breadth#4(tuple#4(@children@3, = [0 0] @children@3 + [0 0] @children@4 + [0 0] @children@6 + [0] @children@4, [1 1] [2 0] [1 1] [2] @children@5, @children@6))] >= [0 0] @children@3 + [0 0] @children@4 + [0] [1 1] [2 0] [0] = [children(@children@3, @children@4, @children@5, @children@6)] [breadth#3(tuple#2(@x, @ys), @queue')] = [1 1] @queue' + [1 0] @ys + [0] [0 0] [0 0] [0] >= [1 1] @queue' + [0] [0 0] [0] = [::(@x, breadth#5(enqueues(@ys, @queue')))] [enqueues(@l, @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueues#1(@l, @queue)] [breadth#5(tuple#2(@breadth@7, @breadth@8))] = [1 1] @breadth@7 + [2 0] @breadth@8 + [0] [0 0] [0 0] [2] >= [1 1] @breadth@7 + [2 0] @breadth@8 + [0] [0 0] [0 0] [2] = [breadth(@breadth@7, @breadth@8)] [children(@a, @b, @l1, @l2)] = [0 0] @a + [0 0] @b + [0] [1 1] [2 0] [0] >= [0 0] @a + [0 0] @b + [0] [1 1] [2 0] [0] = [tuple#2(tuple#2(@a, @b), children#1(@l1, @b, @l2))] [children#1(::(@x, @xs), @b, @l2)] = [0 0] @b + [0] [1 0] [0] >= [0] [0] = [children#3(@l2, @b, @x, @xs)] [children#1(nil(), @b, @l2)] = [0 0] @b + [0] [1 0] [0] >= [0] [0] = [children#2(@l2, @b)] [children#3(::(@y, @ys), @b, @x, @xs)] = [0] [0] >= [0] [0] = [::(tuple#4(@x, @b, nil(), @xs), ::(tuple#4(@x, @y, @xs, @ys), nil()))] [children#3(nil(), @b, @x, @xs)] = [0] [0] >= [0] [0] = [nil()] [children#2(::(@y, @ys), @b)] = [0] [0] >= [0] [0] = [::(tuple#4(@y, @b, nil(), @ys), nil())] [children#2(nil(), @b)] = [0] [0] >= [0] [0] = [nil()] [copyover(@copyover@1, @copyover@2)] = [2 1] @copyover@2 + [0] [2 0] [0] >= [2 0] @copyover@2 + [0] [2 0] [0] = [copyover#1(tuple#2(@copyover@1, @copyover@2))] [copyover#1(tuple#2(@inq, @outq))] = [2 0] @outq + [0] [2 0] [0] >= [2 0] @outq + [0] [2 0] [0] = [copyover#2(@inq, @outq)] [copyover#2(::(@x, @xs), @outq)] = [2 0] @outq + [0] [2 0] [0] >= [2 0] @outq + [0] [2 0] [0] = [copyover(@xs, ::(@x, @outq))] [copyover#2(nil(), @outq)] = [2 0] @outq + [0] [2 0] [0] >= [1 0] @outq + [0] [1 0] [0] = [tuple#2(nil(), @outq)] [dequeue#1(tuple#2(@inq, @outq))] = [0 0] @inq + [0 0] @outq + [0] [1 1] [2 0] [0] >= [0 0] @inq + [0 0] @outq + [0] [1 1] [2 0] [0] = [dequeue#2(@outq, @inq)] [dequeue#2(::(@y, @ys), @inq)] = [0 0] @inq + [0 0] @ys + [0] [1 1] [2 0] [0] >= [0 0] @inq + [0 0] @ys + [0] [1 1] [2 0] [0] = [tuple#2(tuple#2(@inq, @ys), ::(@y, nil()))] [dequeue#2(nil(), @inq)] = [0 0] @inq + [0] [1 1] [0] >= [0] [0] = [dequeue#3(@inq)] [dequeue#3(::(@x, @xs))] = [0] [0] >= [0] [0] = [dequeue#4(copyover(::(@x, @xs), nil()))] [dequeue#3(nil())] = [0] [0] >= [0] [0] = [tuple#2(tuple#2(nil(), nil()), nil())] [dequeue#4(tuple#2(@dequeue@3, @dequeue@4))] = [1 1] @dequeue@3 + [2 0] @dequeue@4 + [0] [2 2] [3 0] [0] >= [0 0] @dequeue@3 + [0 0] @dequeue@4 + [0] [1 1] [2 0] [0] = [dequeue(@dequeue@3, @dequeue@4)] [empty(@x)] = [0] [0] >= [0] [0] = [tuple#2(nil(), nil())] [enqueue(@x, @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueue#1(@queue, @x)] [enqueue#1(tuple#2(@inq, @outq), @x)] = [0 0] @inq + [1 0] @outq + [0] [1 1] [1 0] [0] >= [0 0] @inq + [1 0] @outq + [0] [1 0] [1 0] [0] = [tuple#2(::(@x, @inq), @outq)] [enqueues#1(::(@x, @xs), @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueues(@xs, enqueue(@x, @queue))] [enqueues#1(nil(), @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [@queue] [startBreadth(@xs)] = [2 2] @xs + [2] [2 2] [2] >= [2 2] @xs + [2] [2 0] [2] = [startBreadth#1(@xs)] [startBreadth#1(::(@x, @xs))] = [2 0] @xs + [2] [2 0] [2] > [0] [2] = [startBreadth#2(enqueue(tuple#4(@x, @x, @xs, @xs), empty(#unit())))] [startBreadth#1(nil())] = [2] [2] > [0] [0] = [nil()] [startBreadth#2(tuple#2(@breadth@1, @breadth@2))] = [2 2] @breadth@1 + [4 0] @breadth@2 + [0] [0 0] [2 0] [2] >= [1 1] @breadth@1 + [2 0] @breadth@2 + [0] [0 0] [0 0] [2] = [breadth(@breadth@1, @breadth@2)] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { breadth(@breadth@1, @breadth@2) -> breadth#1(dequeue(@breadth@1, @breadth@2)) , dequeue(@dequeue@1, @dequeue@2) -> dequeue#1(tuple#2(@dequeue@1, @dequeue@2)) , breadth#1(tuple#2(@queue', @elem)) -> breadth#2(@elem, @queue') , breadth#2(::(@z, @_@9), @queue') -> breadth#3(breadth#4(@z), @queue') , breadth#4(tuple#4(@children@3, @children@4, @children@5, @children@6)) -> children(@children@3, @children@4, @children@5, @children@6) , breadth#3(tuple#2(@x, @ys), @queue') -> ::(@x, breadth#5(enqueues(@ys, @queue'))) , enqueues(@l, @queue) -> enqueues#1(@l, @queue) , 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#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() , children#2(::(@y, @ys), @b) -> ::(tuple#4(@y, @b, nil(), @ys), nil()) , children#2(nil(), @b) -> 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#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) , enqueue(@x, @queue) -> enqueue#1(@queue, @x) , enqueue#1(tuple#2(@inq, @outq), @x) -> tuple#2(::(@x, @inq), @outq) , enqueues#1(::(@x, @xs), @queue) -> enqueues(@xs, enqueue(@x, @queue)) , enqueues#1(nil(), @queue) -> @queue , startBreadth(@xs) -> startBreadth#1(@xs) } Weak Trs: { breadth#2(nil(), @queue') -> nil() , empty(@x) -> tuple#2(nil(), nil()) , 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) } Obligation: innermost runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 2' to orient following rules strictly. Trs: { startBreadth(@xs) -> startBreadth#1(@xs) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(breadth#1) = {1}, Uargs(tuple#2) = {2}, Uargs(::) = {2}, Uargs(breadth#3) = {1}, Uargs(enqueues) = {2}, Uargs(breadth#5) = {1}, Uargs(dequeue#4) = {1}, Uargs(enqueue) = {2}, Uargs(startBreadth#2) = {1} TcT has computed following constructor-based matrix interpretation satisfying not(EDA) and not(IDA(1)). [breadth](x1, x2) = [2 0] x2 + [0] [0 0] [1] [dequeue](x1, x2) = [0 0] x2 + [0] [1 0] [0] [breadth#1](x1) = [2 2] x1 + [0] [0 0] [1] [tuple#2](x1, x2) = [0 0] x1 + [1 0] x2 + [0] [1 0] [1 0] [0] [breadth#2](x1, x2) = [2 0] x2 + [0] [0 0] [1] [::](x1, x2) = [1 0] x2 + [0] [0 0] [1] [breadth#4](x1) = [0 0] x1 + [0] [1 1] [1] [breadth#3](x1, x2) = [1 0] x1 + [2 0] x2 + [0] [0 0] [0 0] [1] [nil] = [0] [1] [enqueues](x1, x2) = [1 0] x2 + [0] [0 1] [1] [breadth#5](x1) = [2 0] x1 + [0] [0 0] [1] [tuple#4](x1, x2, x3, x4) = [0 1] x1 + [0 1] x2 + [0 1] x3 + [0 1] x4 + [0] [1 0] [1 0] [1 0] [1 0] [1] [children](x1, x2, x3, x4) = [0 0] x2 + [0] [1 0] [0] [children#1](x1, x2, x3) = [0 0] x1 + [0 0] x2 + [0] [0 2] [1 0] [2] [children#3](x1, x2, x3, x4) = [0] [1] [children#2](x1, x2) = [0] [1] [copyover](x1, x2) = [1 0] x2 + [0] [1 0] [0] [copyover#1](x1) = [1 0] x1 + [0] [1 0] [0] [copyover#2](x1, x2) = [1 0] x2 + [0] [1 0] [0] [dequeue#1](x1) = [0 0] x1 + [0] [1 0] [0] [dequeue#2](x1, x2) = [0 0] x1 + [0] [1 0] [0] [dequeue#3](x1) = [0] [0] [dequeue#4](x1) = [1 2] x1 + [0] [1 0] [0] [empty](x1) = [0] [0] [enqueue](x1, x2) = [1 0] x2 + [0] [0 1] [0] [enqueue#1](x1, x2) = [1 0] x1 + [0] [0 1] [0] [enqueues#1](x1, x2) = [1 0] x2 + [0] [0 1] [1] [startBreadth](x1) = [2 2] x1 + [1] [2 2] [2] [startBreadth#1](x1) = [0 2] x1 + [0] [0 0] [1] [#unit] = [0] [0] [startBreadth#2](x1) = [1 2] x1 + [2] [0 0] [1] This order satisfies following ordering constraints [breadth(@breadth@1, @breadth@2)] = [2 0] @breadth@2 + [0] [0 0] [1] >= [2 0] @breadth@2 + [0] [0 0] [1] = [breadth#1(dequeue(@breadth@1, @breadth@2))] [dequeue(@dequeue@1, @dequeue@2)] = [0 0] @dequeue@2 + [0] [1 0] [0] >= [0 0] @dequeue@2 + [0] [1 0] [0] = [dequeue#1(tuple#2(@dequeue@1, @dequeue@2))] [breadth#1(tuple#2(@queue', @elem))] = [4 0] @elem + [2 0] @queue' + [0] [0 0] [0 0] [1] >= [2 0] @queue' + [0] [0 0] [1] = [breadth#2(@elem, @queue')] [breadth#2(::(@z, @_@9), @queue')] = [2 0] @queue' + [0] [0 0] [1] >= [2 0] @queue' + [0] [0 0] [1] = [breadth#3(breadth#4(@z), @queue')] [breadth#2(nil(), @queue')] = [2 0] @queue' + [0] [0 0] [1] >= [0] [1] = [nil()] [breadth#4(tuple#4(@children@3, = [0 0] @children@3 + [0 0] @children@4 + [0 0] @children@5 + [0 @children@4, 0] @children@6 + [0] @children@5, [1 1] [1 1] [1 1] [1 @children@6))] 1] [2] >= [0 0] @children@4 + [0] [1 0] [0] = [children(@children@3, @children@4, @children@5, @children@6)] [breadth#3(tuple#2(@x, @ys), @queue')] = [2 0] @queue' + [1 0] @ys + [0] [0 0] [0 0] [1] >= [2 0] @queue' + [0] [0 0] [1] = [::(@x, breadth#5(enqueues(@ys, @queue')))] [enqueues(@l, @queue)] = [1 0] @queue + [0] [0 1] [1] >= [1 0] @queue + [0] [0 1] [1] = [enqueues#1(@l, @queue)] [breadth#5(tuple#2(@breadth@7, @breadth@8))] = [2 0] @breadth@8 + [0] [0 0] [1] >= [2 0] @breadth@8 + [0] [0 0] [1] = [breadth(@breadth@7, @breadth@8)] [children(@a, @b, @l1, @l2)] = [0 0] @b + [0] [1 0] [0] >= [0 0] @b + [0] [1 0] [0] = [tuple#2(tuple#2(@a, @b), children#1(@l1, @b, @l2))] [children#1(::(@x, @xs), @b, @l2)] = [0 0] @b + [0] [1 0] [4] >= [0] [1] = [children#3(@l2, @b, @x, @xs)] [children#1(nil(), @b, @l2)] = [0 0] @b + [0] [1 0] [4] >= [0] [1] = [children#2(@l2, @b)] [children#3(::(@y, @ys), @b, @x, @xs)] = [0] [1] >= [0] [1] = [::(tuple#4(@x, @b, nil(), @xs), ::(tuple#4(@x, @y, @xs, @ys), nil()))] [children#3(nil(), @b, @x, @xs)] = [0] [1] >= [0] [1] = [nil()] [children#2(::(@y, @ys), @b)] = [0] [1] >= [0] [1] = [::(tuple#4(@y, @b, nil(), @ys), nil())] [children#2(nil(), @b)] = [0] [1] >= [0] [1] = [nil()] [copyover(@copyover@1, @copyover@2)] = [1 0] @copyover@2 + [0] [1 0] [0] >= [1 0] @copyover@2 + [0] [1 0] [0] = [copyover#1(tuple#2(@copyover@1, @copyover@2))] [copyover#1(tuple#2(@inq, @outq))] = [1 0] @outq + [0] [1 0] [0] >= [1 0] @outq + [0] [1 0] [0] = [copyover#2(@inq, @outq)] [copyover#2(::(@x, @xs), @outq)] = [1 0] @outq + [0] [1 0] [0] >= [1 0] @outq + [0] [1 0] [0] = [copyover(@xs, ::(@x, @outq))] [copyover#2(nil(), @outq)] = [1 0] @outq + [0] [1 0] [0] >= [1 0] @outq + [0] [1 0] [0] = [tuple#2(nil(), @outq)] [dequeue#1(tuple#2(@inq, @outq))] = [0 0] @outq + [0] [1 0] [0] >= [0 0] @outq + [0] [1 0] [0] = [dequeue#2(@outq, @inq)] [dequeue#2(::(@y, @ys), @inq)] = [0 0] @ys + [0] [1 0] [0] >= [0 0] @ys + [0] [1 0] [0] = [tuple#2(tuple#2(@inq, @ys), ::(@y, nil()))] [dequeue#2(nil(), @inq)] = [0] [0] >= [0] [0] = [dequeue#3(@inq)] [dequeue#3(::(@x, @xs))] = [0] [0] >= [0] [0] = [dequeue#4(copyover(::(@x, @xs), nil()))] [dequeue#3(nil())] = [0] [0] >= [0] [0] = [tuple#2(tuple#2(nil(), nil()), nil())] [dequeue#4(tuple#2(@dequeue@3, @dequeue@4))] = [2 0] @dequeue@3 + [3 0] @dequeue@4 + [0] [0 0] [1 0] [0] >= [0 0] @dequeue@4 + [0] [1 0] [0] = [dequeue(@dequeue@3, @dequeue@4)] [empty(@x)] = [0] [0] >= [0] [0] = [tuple#2(nil(), nil())] [enqueue(@x, @queue)] = [1 0] @queue + [0] [0 1] [0] >= [1 0] @queue + [0] [0 1] [0] = [enqueue#1(@queue, @x)] [enqueue#1(tuple#2(@inq, @outq), @x)] = [0 0] @inq + [1 0] @outq + [0] [1 0] [1 0] [0] >= [0 0] @inq + [1 0] @outq + [0] [1 0] [1 0] [0] = [tuple#2(::(@x, @inq), @outq)] [enqueues#1(::(@x, @xs), @queue)] = [1 0] @queue + [0] [0 1] [1] >= [1 0] @queue + [0] [0 1] [1] = [enqueues(@xs, enqueue(@x, @queue))] [enqueues#1(nil(), @queue)] = [1 0] @queue + [0] [0 1] [1] >= [1 0] @queue + [0] [0 1] [0] = [@queue] [startBreadth(@xs)] = [2 2] @xs + [1] [2 2] [2] > [0 2] @xs + [0] [0 0] [1] = [startBreadth#1(@xs)] [startBreadth#1(::(@x, @xs))] = [2] [1] >= [2] [1] = [startBreadth#2(enqueue(tuple#4(@x, @x, @xs, @xs), empty(#unit())))] [startBreadth#1(nil())] = [2] [1] > [0] [1] = [nil()] [startBreadth#2(tuple#2(@breadth@1, @breadth@2))] = [2 0] @breadth@1 + [3 0] @breadth@2 + [2] [0 0] [0 0] [1] > [2 0] @breadth@2 + [0] [0 0] [1] = [breadth(@breadth@1, @breadth@2)] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { breadth(@breadth@1, @breadth@2) -> breadth#1(dequeue(@breadth@1, @breadth@2)) , dequeue(@dequeue@1, @dequeue@2) -> dequeue#1(tuple#2(@dequeue@1, @dequeue@2)) , breadth#1(tuple#2(@queue', @elem)) -> breadth#2(@elem, @queue') , breadth#2(::(@z, @_@9), @queue') -> breadth#3(breadth#4(@z), @queue') , breadth#4(tuple#4(@children@3, @children@4, @children@5, @children@6)) -> children(@children@3, @children@4, @children@5, @children@6) , breadth#3(tuple#2(@x, @ys), @queue') -> ::(@x, breadth#5(enqueues(@ys, @queue'))) , enqueues(@l, @queue) -> enqueues#1(@l, @queue) , 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#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() , children#2(::(@y, @ys), @b) -> ::(tuple#4(@y, @b, nil(), @ys), nil()) , children#2(nil(), @b) -> 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#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) , enqueue(@x, @queue) -> enqueue#1(@queue, @x) , enqueue#1(tuple#2(@inq, @outq), @x) -> tuple#2(::(@x, @inq), @outq) , enqueues#1(::(@x, @xs), @queue) -> enqueues(@xs, enqueue(@x, @queue)) , enqueues#1(nil(), @queue) -> @queue } Weak Trs: { breadth#2(nil(), @queue') -> nil() , empty(@x) -> tuple#2(nil(), nil()) , 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) } Obligation: innermost runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'trivial' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Sequentially' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Polynomial Path Order' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..