Problem Transformed CSR 04 Ex1 GL02a GM

Tool CaT

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 GL02a GM

stdout:

MAYBE

Problem:
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)

Proof:
Open

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 GL02a GM

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex1 GL02a GM

stdout:

YES(?,O(n^1))

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           YES(?,O(n^1))
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  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)}

Proof Output:
  'matrix-interpretation of dimension 1' proved the best result:

  Details:
  --------
    'matrix-interpretation of dimension 1' succeeded with the following output:
     'matrix-interpretation of dimension 1'
     --------------------------------------
     Answer:           YES(?,O(n^1))
     Input Problem:    innermost runtime-complexity with respect to
       Rules:
         {  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)}

     Proof Output:
       The following argument positions are usable:
         Uargs(a__eq) = {}, Uargs(s) = {}, Uargs(a__inf) = {1},
         Uargs(cons) = {}, Uargs(inf) = {}, Uargs(a__take) = {1, 2},
         Uargs(take) = {}, Uargs(a__length) = {1}, Uargs(length) = {},
         Uargs(mark) = {}, Uargs(eq) = {}
       We have the following constructor-restricted matrix interpretation:
       Interpretation Functions:
        a__eq(x1, x2) = [2] x1 + [0] x2 + [4]
        0() = [2]
        true() = [1]
        s(x1) = [1] x1 + [1]
        false() = [0]
        a__inf(x1) = [1] x1 + [4]
        cons(x1, x2) = [0] x1 + [1] x2 + [0]
        inf(x1) = [1] x1 + [2]
        a__take(x1, x2) = [1] x1 + [1] x2 + [2]
        nil() = [2]
        take(x1, x2) = [1] x1 + [1] x2 + [1]
        a__length(x1) = [1] x1 + [6]
        length(x1) = [1] x1 + [2]
        mark(x1) = [4] x1 + [1]
        eq(x1, x2) = [1] x1 + [0] x2 + [2]

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 Ex1 GL02a GM

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 Ex1 GL02a GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  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)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds