interpretations
TIMEOUT
We are left with following problem, upon which TcT provides the
certificate TIMEOUT.
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, replace(N, M, nil()) -> nil()
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, selsort(nil()) -> nil()
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) }
Obligation:
innermost runtime complexity
Answer:
TIMEOUT
Computation stopped due to timeout after 20.0 seconds.
Arrrr..
lmpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, nil()) -> nil()
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(nil()) -> nil()
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
mpo
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, nil()) -> nil()
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(nil()) -> nil()
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, nil()) -> nil()
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(nil()) -> nil()
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..
popstar-ps
MAYBE
We are left with following problem, upon which TcT provides the
certificate MAYBE.
Strict Trs:
{ eq(0(), 0()) -> true()
, eq(0(), s(Y)) -> false()
, eq(s(X), 0()) -> false()
, eq(s(X), s(Y)) -> eq(X, Y)
, le(0(), Y) -> true()
, le(s(X), 0()) -> false()
, le(s(X), s(Y)) -> le(X, Y)
, min(cons(0(), nil())) -> 0()
, min(cons(s(N), nil())) -> s(N)
, min(cons(N, cons(M, L))) -> ifmin(le(N, M), cons(N, cons(M, L)))
, ifmin(true(), cons(N, cons(M, L))) -> min(cons(N, L))
, ifmin(false(), cons(N, cons(M, L))) -> min(cons(M, L))
, replace(N, M, nil()) -> nil()
, replace(N, M, cons(K, L)) -> ifrepl(eq(N, K), N, M, cons(K, L))
, ifrepl(true(), N, M, cons(K, L)) -> cons(M, L)
, ifrepl(false(), N, M, cons(K, L)) -> cons(K, replace(N, M, L))
, selsort(nil()) -> nil()
, selsort(cons(N, L)) ->
ifselsort(eq(N, min(cons(N, L))), cons(N, L))
, ifselsort(true(), cons(N, L)) -> cons(N, selsort(L))
, ifselsort(false(), cons(N, L)) ->
cons(min(cons(N, L)), selsort(replace(min(cons(N, L)), N, L))) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..