LMPO
MAYBE
We consider the following Problem:
Strict Trs:
{ isLeaf(leaf()) -> true()
, isLeaf(cons(u, v)) -> false()
, left(cons(u, v)) -> u
, right(cons(u, v)) -> v
, concat(leaf(), y) -> y
, concat(cons(u, v), y) -> cons(u, concat(v, y))
, less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
, if1(b, true(), u, v) -> false()
, if1(b, false(), u, v) -> if2(b, u, v)
, if2(true(), u, v) -> true()
, if2(false(), u, v) ->
less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
MPO
MAYBE
We consider the following Problem:
Strict Trs:
{ isLeaf(leaf()) -> true()
, isLeaf(cons(u, v)) -> false()
, left(cons(u, v)) -> u
, right(cons(u, v)) -> v
, concat(leaf(), y) -> y
, concat(cons(u, v), y) -> cons(u, concat(v, y))
, less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
, if1(b, true(), u, v) -> false()
, if1(b, false(), u, v) -> if2(b, u, v)
, if2(true(), u, v) -> true()
, if2(false(), u, v) ->
less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..
POP*
MAYBE
We consider the following Problem:
Strict Trs:
{ isLeaf(leaf()) -> true()
, isLeaf(cons(u, v)) -> false()
, left(cons(u, v)) -> u
, right(cons(u, v)) -> v
, concat(leaf(), y) -> y
, concat(cons(u, v), y) -> cons(u, concat(v, y))
, less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
, if1(b, true(), u, v) -> false()
, if1(b, false(), u, v) -> if2(b, u, v)
, if2(true(), u, v) -> true()
, if2(false(), u, v) ->
less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
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:
{ isLeaf(leaf()) -> true()
, isLeaf(cons(u, v)) -> false()
, left(cons(u, v)) -> u
, right(cons(u, v)) -> v
, concat(leaf(), y) -> y
, concat(cons(u, v), y) -> cons(u, concat(v, y))
, less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
, if1(b, true(), u, v) -> false()
, if1(b, false(), u, v) -> if2(b, u, v)
, if2(true(), u, v) -> true()
, if2(false(), u, v) ->
less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
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:
{ isLeaf(leaf()) -> true()
, isLeaf(cons(u, v)) -> false()
, left(cons(u, v)) -> u
, right(cons(u, v)) -> v
, concat(leaf(), y) -> y
, concat(cons(u, v), y) -> cons(u, concat(v, y))
, less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
, if1(b, true(), u, v) -> false()
, if1(b, false(), u, v) -> if2(b, u, v)
, if2(true(), u, v) -> true()
, if2(false(), u, v) ->
less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
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:
{ isLeaf(leaf()) -> true()
, isLeaf(cons(u, v)) -> false()
, left(cons(u, v)) -> u
, right(cons(u, v)) -> v
, concat(leaf(), y) -> y
, concat(cons(u, v), y) -> cons(u, concat(v, y))
, less_leaves(u, v) -> if1(isLeaf(u), isLeaf(v), u, v)
, if1(b, true(), u, v) -> false()
, if1(b, false(), u, v) -> if2(b, u, v)
, if2(true(), u, v) -> true()
, if2(false(), u, v) ->
less_leaves(concat(left(u), right(u)), concat(left(v), right(v)))}
StartTerms: basic terms
Strategy: innermost
Certificate: MAYBE
Proof:
The input cannot be shown compatible
Arrrr..