Problem Rubio 04 bintrees

MAYBE

We consider the following Problem:

  Strict Trs:
    {  concat(leaf(), Y) -> Y
     , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
     , lessleaves(X, leaf()) -> false()
     , lessleaves(leaf(), cons(W, Z)) -> true()
     , lessleaves(cons(U, V), cons(W, Z)) ->
       lessleaves(concat(U, V), concat(W, Z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  concat(leaf(), Y) -> Y
     , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
     , lessleaves(X, leaf()) -> false()
     , lessleaves(leaf(), cons(W, Z)) -> true()
     , lessleaves(cons(U, V), cons(W, Z)) ->
       lessleaves(concat(U, V), concat(W, Z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  concat(leaf(), Y) -> Y
     , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
     , lessleaves(X, leaf()) -> false()
     , lessleaves(leaf(), cons(W, Z)) -> true()
     , lessleaves(cons(U, V), cons(W, Z)) ->
       lessleaves(concat(U, V), concat(W, Z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  concat(leaf(), Y) -> Y
     , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
     , lessleaves(X, leaf()) -> false()
     , lessleaves(leaf(), cons(W, Z)) -> true()
     , lessleaves(cons(U, V), cons(W, Z)) ->
       lessleaves(concat(U, V), concat(W, Z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  concat(leaf(), Y) -> Y
     , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
     , lessleaves(X, leaf()) -> false()
     , lessleaves(leaf(), cons(W, Z)) -> true()
     , lessleaves(cons(U, V), cons(W, Z)) ->
       lessleaves(concat(U, V), concat(W, Z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  concat(leaf(), Y) -> Y
     , concat(cons(U, V), Y) -> cons(U, concat(V, Y))
     , lessleaves(X, leaf()) -> false()
     , lessleaves(leaf(), cons(W, Z)) -> true()
     , lessleaves(cons(U, V), cons(W, Z)) ->
       lessleaves(concat(U, V), concat(W, Z))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..