LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ isEmpty(empty()) -> true()
, isEmpty(node(l, r)) -> false()
, left(empty()) -> empty()
, left(node(l, r)) -> l
, right(empty()) -> empty()
, right(node(l, r)) -> r
, inc(0()) -> s(0())
, inc(s(x)) -> s(inc(x))
, count(n, x) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)), node(right(left(n)), right(n))),
x,
inc(x))
, if(true(), b, n, m, x, y) -> x
, if(false(), false(), n, m, x, y) -> count(m, x)
, if(false(), true(), n, m, x, y) -> count(n, y)
, nrOfNodes(n) -> count(n, 0())}
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, r)) -> false()
, left(empty()) -> empty()
, left(node(l, r)) -> l
, right(empty()) -> empty()
, right(node(l, r)) -> r
, inc(0()) -> s(0())
, inc(s(x)) -> s(inc(x))
, count(n, x) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)), node(right(left(n)), right(n))),
x,
inc(x))
, if(true(), b, n, m, x, y) -> x
, if(false(), false(), n, m, x, y) -> count(m, x)
, if(false(), true(), n, m, x, y) -> count(n, y)
, nrOfNodes(n) -> count(n, 0())}
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, r)) -> false()
, left(empty()) -> empty()
, left(node(l, r)) -> l
, right(empty()) -> empty()
, right(node(l, r)) -> r
, inc(0()) -> s(0())
, inc(s(x)) -> s(inc(x))
, count(n, x) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)), node(right(left(n)), right(n))),
x,
inc(x))
, if(true(), b, n, m, x, y) -> x
, if(false(), false(), n, m, x, y) -> count(m, x)
, if(false(), true(), n, m, x, y) -> count(n, y)
, nrOfNodes(n) -> count(n, 0())}
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, r)) -> false()
, left(empty()) -> empty()
, left(node(l, r)) -> l
, right(empty()) -> empty()
, right(node(l, r)) -> r
, inc(0()) -> s(0())
, inc(s(x)) -> s(inc(x))
, count(n, x) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)), node(right(left(n)), right(n))),
x,
inc(x))
, if(true(), b, n, m, x, y) -> x
, if(false(), false(), n, m, x, y) -> count(m, x)
, if(false(), true(), n, m, x, y) -> count(n, y)
, nrOfNodes(n) -> count(n, 0())}
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, r)) -> false()
, left(empty()) -> empty()
, left(node(l, r)) -> l
, right(empty()) -> empty()
, right(node(l, r)) -> r
, inc(0()) -> s(0())
, inc(s(x)) -> s(inc(x))
, count(n, x) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)), node(right(left(n)), right(n))),
x,
inc(x))
, if(true(), b, n, m, x, y) -> x
, if(false(), false(), n, m, x, y) -> count(m, x)
, if(false(), true(), n, m, x, y) -> count(n, y)
, nrOfNodes(n) -> count(n, 0())}
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, r)) -> false()
, left(empty()) -> empty()
, left(node(l, r)) -> l
, right(empty()) -> empty()
, right(node(l, r)) -> r
, inc(0()) -> s(0())
, inc(s(x)) -> s(inc(x))
, count(n, x) ->
if(isEmpty(n),
isEmpty(left(n)),
right(n),
node(left(left(n)), node(right(left(n)), right(n))),
x,
inc(x))
, if(true(), b, n, m, x, y) -> x
, if(false(), false(), n, m, x, y) -> count(m, x)
, if(false(), true(), n, m, x, y) -> count(n, y)
, nrOfNodes(n) -> count(n, 0())}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..