Problem AProVE 10 ex1

MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(x, y) -> cond(lt(x, y), x, y)
     , cond(tt(), x, y) -> f(s(x), s(y))
     , lt(0(), y) -> tt()
     , lt(s(x), s(y)) -> lt(x, y)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(x, y) -> cond(lt(x, y), x, y)
     , cond(tt(), x, y) -> f(s(x), s(y))
     , lt(0(), y) -> tt()
     , lt(s(x), s(y)) -> lt(x, y)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(x, y) -> cond(lt(x, y), x, y)
     , cond(tt(), x, y) -> f(s(x), s(y))
     , lt(0(), y) -> tt()
     , lt(s(x), s(y)) -> lt(x, y)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(x, y) -> cond(lt(x, y), x, y)
     , cond(tt(), x, y) -> f(s(x), s(y))
     , lt(0(), y) -> tt()
     , lt(s(x), s(y)) -> lt(x, y)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(x, y) -> cond(lt(x, y), x, y)
     , cond(tt(), x, y) -> f(s(x), s(y))
     , lt(0(), y) -> tt()
     , lt(s(x), s(y)) -> lt(x, y)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  f(x, y) -> cond(lt(x, y), x, y)
     , cond(tt(), x, y) -> f(s(x), s(y))
     , lt(0(), y) -> tt()
     , lt(s(x), s(y)) -> lt(x, y)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..