Problem queue.raml

tct

Execution Time (secs)
60.107
Answer
TIMEOUT
Inputqueue.raml
TIMEOUT

We are left with following problem, upon which TcT provides the
certificate TIMEOUT.

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:
  TIMEOUT

Computation stopped due to timeout after 60.0 seconds.

Arrrr..

tct-popstar

Execution Time (secs)
60.248
Answer
TIMEOUT
Inputqueue.raml
TIMEOUT

We are left with following problem, upon which TcT provides the
certificate TIMEOUT.

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:
  TIMEOUT

Computation stopped due to timeout after 60.0 seconds.

Arrrr..