Problem Secret 07 TRS aprove03

TIMEOUT

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

Strict Trs:
  { average(x, y) -> if(ge(x, y), x, y)
  , if(true(), x, y) -> averIter(y, x, y)
  , if(false(), x, y) -> averIter(x, y, x)
  , ge(x, 0()) -> true()
  , ge(s(x), s(y)) -> ge(x, y)
  , ge(0(), s(y)) -> false()
  , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z)
  , ifIter(true(), x, y, z) -> z
  , ifIter(false(), x, y, z) ->
    averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0())))
  , plus(s(x), y) -> s(plus(x, y))
  , plus(0(), y) -> y
  , append(nil(), y) -> y
  , append(cons(n, x), y) -> cons(n, app(x, y))
  , low(n, nil()) -> nil()
  , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x))
  , if_low(true(), n, cons(m, x)) -> low(n, x)
  , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x))
  , high(n, nil()) -> nil()
  , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x))
  , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x))
  , if_high(false(), n, cons(m, x)) -> high(n, x)
  , quicksort(x) -> ifquick(isempty(x), x)
  , ifquick(true(), x) -> nil()
  , ifquick(false(), x) ->
    append(quicksort(low(head(x), tail(x))),
           cons(tail(x), quicksort(high(head(x), tail(x)))))
  , isempty(nil()) -> true()
  , isempty(cons(n, x)) -> false()
  , head(nil()) -> error()
  , head(cons(n, x)) -> n
  , tail(nil()) -> nil()
  , tail(cons(n, x)) -> x
  , a() -> b()
  , a() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  TIMEOUT

Computation stopped due to timeout after 20.0 seconds.

Arrrr..

MAYBE

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

Strict Trs:
  { average(x, y) -> if(ge(x, y), x, y)
  , if(true(), x, y) -> averIter(y, x, y)
  , if(false(), x, y) -> averIter(x, y, x)
  , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z)
  , ifIter(true(), x, y, z) -> z
  , ifIter(false(), x, y, z) ->
    averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0())))
  , append(nil(), y) -> y
  , append(cons(n, x), y) -> cons(n, app(x, y))
  , low(n, nil()) -> nil()
  , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x))
  , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x))
  , if_low(true(), n, cons(m, x)) -> low(n, x)
  , high(n, nil()) -> nil()
  , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x))
  , if_high(false(), n, cons(m, x)) -> high(n, x)
  , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x))
  , quicksort(x) -> ifquick(isempty(x), x)
  , ifquick(true(), x) -> nil()
  , ifquick(false(), x) ->
    append(quicksort(low(head(x), tail(x))),
           cons(tail(x), quicksort(high(head(x), tail(x)))))
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , isempty(nil()) -> true()
  , isempty(cons(n, x)) -> false()
  , head(nil()) -> error()
  , head(cons(n, x)) -> n
  , tail(nil()) -> nil()
  , tail(cons(n, x)) -> x
  , ge(x, 0()) -> true()
  , ge(0(), s(y)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , a() -> b()
  , a() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { average(x, y) -> if(ge(x, y), x, y)
  , if(true(), x, y) -> averIter(y, x, y)
  , if(false(), x, y) -> averIter(x, y, x)
  , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z)
  , ifIter(true(), x, y, z) -> z
  , ifIter(false(), x, y, z) ->
    averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0())))
  , append(nil(), y) -> y
  , append(cons(n, x), y) -> cons(n, app(x, y))
  , low(n, nil()) -> nil()
  , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x))
  , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x))
  , if_low(true(), n, cons(m, x)) -> low(n, x)
  , high(n, nil()) -> nil()
  , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x))
  , if_high(false(), n, cons(m, x)) -> high(n, x)
  , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x))
  , quicksort(x) -> ifquick(isempty(x), x)
  , ifquick(true(), x) -> nil()
  , ifquick(false(), x) ->
    append(quicksort(low(head(x), tail(x))),
           cons(tail(x), quicksort(high(head(x), tail(x)))))
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , isempty(nil()) -> true()
  , isempty(cons(n, x)) -> false()
  , head(nil()) -> error()
  , head(cons(n, x)) -> n
  , tail(nil()) -> nil()
  , tail(cons(n, x)) -> x
  , ge(x, 0()) -> true()
  , ge(0(), s(y)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , a() -> b()
  , a() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { average(x, y) -> if(ge(x, y), x, y)
  , if(true(), x, y) -> averIter(y, x, y)
  , if(false(), x, y) -> averIter(x, y, x)
  , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z)
  , ifIter(true(), x, y, z) -> z
  , ifIter(false(), x, y, z) ->
    averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0())))
  , append(nil(), y) -> y
  , append(cons(n, x), y) -> cons(n, app(x, y))
  , low(n, nil()) -> nil()
  , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x))
  , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x))
  , if_low(true(), n, cons(m, x)) -> low(n, x)
  , high(n, nil()) -> nil()
  , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x))
  , if_high(false(), n, cons(m, x)) -> high(n, x)
  , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x))
  , quicksort(x) -> ifquick(isempty(x), x)
  , ifquick(true(), x) -> nil()
  , ifquick(false(), x) ->
    append(quicksort(low(head(x), tail(x))),
           cons(tail(x), quicksort(high(head(x), tail(x)))))
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , isempty(nil()) -> true()
  , isempty(cons(n, x)) -> false()
  , head(nil()) -> error()
  , head(cons(n, x)) -> n
  , tail(nil()) -> nil()
  , tail(cons(n, x)) -> x
  , ge(x, 0()) -> true()
  , ge(0(), s(y)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , a() -> b()
  , a() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..

MAYBE

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

Strict Trs:
  { average(x, y) -> if(ge(x, y), x, y)
  , if(true(), x, y) -> averIter(y, x, y)
  , if(false(), x, y) -> averIter(x, y, x)
  , averIter(x, y, z) -> ifIter(ge(x, y), x, y, z)
  , ifIter(true(), x, y, z) -> z
  , ifIter(false(), x, y, z) ->
    averIter(plus(x, s(s(s(0())))), plus(y, s(0())), plus(z, s(0())))
  , append(nil(), y) -> y
  , append(cons(n, x), y) -> cons(n, app(x, y))
  , low(n, nil()) -> nil()
  , low(n, cons(m, x)) -> if_low(ge(m, n), n, cons(m, x))
  , if_low(false(), n, cons(m, x)) -> cons(m, low(n, x))
  , if_low(true(), n, cons(m, x)) -> low(n, x)
  , high(n, nil()) -> nil()
  , high(n, cons(m, x)) -> if_high(ge(m, n), n, cons(m, x))
  , if_high(false(), n, cons(m, x)) -> high(n, x)
  , if_high(true(), n, cons(m, x)) -> cons(average(m, m), high(n, x))
  , quicksort(x) -> ifquick(isempty(x), x)
  , ifquick(true(), x) -> nil()
  , ifquick(false(), x) ->
    append(quicksort(low(head(x), tail(x))),
           cons(tail(x), quicksort(high(head(x), tail(x)))))
  , plus(0(), y) -> y
  , plus(s(x), y) -> s(plus(x, y))
  , isempty(nil()) -> true()
  , isempty(cons(n, x)) -> false()
  , head(nil()) -> error()
  , head(cons(n, x)) -> n
  , tail(nil()) -> nil()
  , tail(cons(n, x)) -> x
  , ge(x, 0()) -> true()
  , ge(0(), s(y)) -> false()
  , ge(s(x), s(y)) -> ge(x, y)
  , a() -> b()
  , a() -> c() }
Obligation:
  innermost runtime complexity
Answer:
  MAYBE

The input cannot be shown compatible

Arrrr..