Problem Transformed CSR 04 Ex1 GL02a GM

YES(?,ELEMENTARY)

We consider the following Problem:

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

Certificate: YES(?,ELEMENTARY)

Proof:
  The input was oriented with the instance of
  Lightweight Multiset Path Order () as induced by the safe mapping
  
   safe(a__eq) = {}, safe(0) = {}, safe(true) = {}, safe(s) = {1},
   safe(false) = {}, safe(a__inf) = {1}, safe(cons) = {1, 2},
   safe(inf) = {1}, safe(a__take) = {1, 2}, safe(nil) = {},
   safe(take) = {1, 2}, safe(a__length) = {1}, safe(length) = {1},
   safe(mark) = {}, safe(eq) = {1, 2}
  
  and precedence
  
   mark > a__eq, mark > a__inf, mark > a__take, mark > a__length .
  
  Following symbols are considered recursive:
  
   {a__eq, a__inf, a__take, a__length, mark}
  
  The recursion depth is 2 .
  
  For your convenience, here are the oriented rules in predicative
  notation (possibly applying argument filtering):
  
   Strict DPs: {}
   Weak DPs  : {}
   Strict Trs:
     {  a__eq(0(), 0();) -> true()
      , a__eq(s(; X), s(; Y);) -> a__eq(X, Y;)
      , a__eq(X, Y;) -> false()
      , a__inf(; X) -> cons(; X, inf(; s(; X)))
      , a__take(; 0(), X) -> nil()
      , a__take(; s(; X), cons(; Y, L)) -> cons(; Y, take(; X, L))
      , a__length(; nil()) -> 0()
      , a__length(; cons(; X, L)) -> s(; length(; L))
      , mark(eq(; X1, X2);) -> a__eq(X1, X2;)
      , mark(inf(; X);) -> a__inf(; mark(X;))
      , mark(take(; X1, X2);) -> a__take(; mark(X1;), mark(X2;))
      , mark(length(; X);) -> a__length(; mark(X;))
      , mark(0();) -> 0()
      , mark(true();) -> true()
      , mark(s(; X);) -> s(; X)
      , mark(false();) -> false()
      , mark(cons(; X1, X2);) -> cons(; X1, X2)
      , mark(nil();) -> nil()
      , a__eq(X1, X2;) -> eq(; X1, X2)
      , a__inf(; X) -> inf(; X)
      , a__take(; X1, X2) -> take(; X1, X2)
      , a__length(; X) -> length(; X)}
   Weak Trs  : {}

Hurray, we answered YES(?,ELEMENTARY)

YES(?,PRIMREC)

We consider the following Problem:

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

Certificate: YES(?,PRIMREC)

Proof:
  The input was oriented with the instance of
  'multiset path orders' as induced by the precedence
  
   a__eq > false, a__eq > eq, 0 > true, a__inf > s, a__inf > cons,
   a__inf > inf, a__take > cons, a__take > take, a__length > s,
   a__length > length, mark > a__eq, mark > a__inf, mark > a__take,
   mark > a__length, 0 ~ nil .

Hurray, we answered YES(?,PRIMREC)

MAYBE

We consider the following Problem:

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

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

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

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

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

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..

MAYBE

We consider the following Problem:

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

Certificate: MAYBE

Proof:
  The input cannot be shown compatible

Arrrr..