interpretations
TIMEOUT
We are left with following problem, upon which TcT provides the
certificate TIMEOUT.
Strict Trs:
{ isEmpty(empty()) -> true()
, isEmpty(node(l, x, r)) -> false()
, left(empty()) -> empty()
, left(node(l, x, r)) -> l
, right(empty()) -> empty()
, right(node(l, x, r)) -> r
, elem(node(l, x, r)) -> x
, append(nil(), x) -> cons(x, nil())
, append(cons(y(), ys), x) -> cons(y(), append(ys, x))
, listify(n, xs) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)),
elem(left(n)),
node(right(left(n)), elem(n), right(n))),
xs,
append(xs, n))
, if(true(), b, n, m, xs, ys) -> xs
, if(false(), true(), n, m, xs, ys) -> listify(n, ys)
, if(false(), false(), n, m, xs, ys) -> listify(m, xs)
, toList(n) -> listify(n, nil()) }
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:
{ isEmpty(empty()) -> true()
, isEmpty(node(l, x, r)) -> false()
, left(empty()) -> empty()
, left(node(l, x, r)) -> l
, right(empty()) -> empty()
, right(node(l, x, r)) -> r
, elem(node(l, x, r)) -> x
, append(nil(), x) -> cons(x, nil())
, append(cons(y(), ys), x) -> cons(y(), append(ys, x))
, listify(n, xs) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)),
elem(left(n)),
node(right(left(n)), elem(n), right(n))),
xs,
append(xs, n))
, if(true(), b, n, m, xs, ys) -> xs
, if(false(), false(), n, m, xs, ys) -> listify(m, xs)
, if(false(), true(), n, m, xs, ys) -> listify(n, ys)
, toList(n) -> listify(n, nil()) }
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:
{ isEmpty(empty()) -> true()
, isEmpty(node(l, x, r)) -> false()
, left(empty()) -> empty()
, left(node(l, x, r)) -> l
, right(empty()) -> empty()
, right(node(l, x, r)) -> r
, elem(node(l, x, r)) -> x
, append(nil(), x) -> cons(x, nil())
, append(cons(y(), ys), x) -> cons(y(), append(ys, x))
, listify(n, xs) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)),
elem(left(n)),
node(right(left(n)), elem(n), right(n))),
xs,
append(xs, n))
, if(true(), b, n, m, xs, ys) -> xs
, if(false(), false(), n, m, xs, ys) -> listify(m, xs)
, if(false(), true(), n, m, xs, ys) -> listify(n, ys)
, toList(n) -> listify(n, nil()) }
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:
{ isEmpty(empty()) -> true()
, isEmpty(node(l, x, r)) -> false()
, left(empty()) -> empty()
, left(node(l, x, r)) -> l
, right(empty()) -> empty()
, right(node(l, x, r)) -> r
, elem(node(l, x, r)) -> x
, append(nil(), x) -> cons(x, nil())
, append(cons(y(), ys), x) -> cons(y(), append(ys, x))
, listify(n, xs) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)),
elem(left(n)),
node(right(left(n)), elem(n), right(n))),
xs,
append(xs, n))
, if(true(), b, n, m, xs, ys) -> xs
, if(false(), false(), n, m, xs, ys) -> listify(m, xs)
, if(false(), true(), n, m, xs, ys) -> listify(n, ys)
, toList(n) -> listify(n, nil()) }
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:
{ isEmpty(empty()) -> true()
, isEmpty(node(l, x, r)) -> false()
, left(empty()) -> empty()
, left(node(l, x, r)) -> l
, right(empty()) -> empty()
, right(node(l, x, r)) -> r
, elem(node(l, x, r)) -> x
, append(nil(), x) -> cons(x, nil())
, append(cons(y(), ys), x) -> cons(y(), append(ys, x))
, listify(n, xs) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)),
elem(left(n)),
node(right(left(n)), elem(n), right(n))),
xs,
append(xs, n))
, if(true(), b, n, m, xs, ys) -> xs
, if(false(), false(), n, m, xs, ys) -> listify(m, xs)
, if(false(), true(), n, m, xs, ys) -> listify(n, ys)
, toList(n) -> listify(n, nil()) }
Obligation:
innermost runtime complexity
Answer:
MAYBE
The input cannot be shown compatible
Arrrr..