Problem CSR 04 Ex1 GL02a

MAYBE

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(s(X), s(Y)) -> eq(X, Y)
     , eq(X, Y) -> false()
     , inf(X) -> cons(X, inf(s(X)))
     , take(0(), X) -> nil()
     , take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
     , length(nil()) -> 0()
     , length(cons(X, L)) -> s(length(L))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(s(X), s(Y)) -> eq(X, Y)
     , eq(X, Y) -> false()
     , inf(X) -> cons(X, inf(s(X)))
     , take(0(), X) -> nil()
     , take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
     , length(nil()) -> 0()
     , length(cons(X, L)) -> s(length(L))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(s(X), s(Y)) -> eq(X, Y)
     , eq(X, Y) -> false()
     , inf(X) -> cons(X, inf(s(X)))
     , take(0(), X) -> nil()
     , take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
     , length(nil()) -> 0()
     , length(cons(X, L)) -> s(length(L))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(s(X), s(Y)) -> eq(X, Y)
     , eq(X, Y) -> false()
     , inf(X) -> cons(X, inf(s(X)))
     , take(0(), X) -> nil()
     , take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
     , length(nil()) -> 0()
     , length(cons(X, L)) -> s(length(L))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(s(X), s(Y)) -> eq(X, Y)
     , eq(X, Y) -> false()
     , inf(X) -> cons(X, inf(s(X)))
     , take(0(), X) -> nil()
     , take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
     , length(nil()) -> 0()
     , length(cons(X, L)) -> s(length(L))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

  Strict Trs:
    {  eq(0(), 0()) -> true()
     , eq(s(X), s(Y)) -> eq(X, Y)
     , eq(X, Y) -> false()
     , inf(X) -> cons(X, inf(s(X)))
     , take(0(), X) -> nil()
     , take(s(X), cons(Y, L)) -> cons(Y, take(X, L))
     , length(nil()) -> 0()
     , length(cons(X, L)) -> s(length(L))}
  StartTerms: basic terms
  Strategy: innermost

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..