LMPO
MAYBE
We consider the following Problem:
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())}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
MAYBE
We consider the following Problem:
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())}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
MAYBE
We consider the following Problem:
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())}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP* (PS)
MAYBE
We consider the following Problem:
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())}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP*
MAYBE
We consider the following Problem:
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())}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
Small POP* (PS)
MAYBE
We consider the following Problem:
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())}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..