Problem Transformed CSR 04 ExIntrod GM04 GM

Tool CaT

Execution Time	Unknown
Answer	YES(?,O(n^3))
Input	Transformed CSR 04 ExIntrod GM04 GM

stdout:

YES(?,O(n^3))

Problem:
a__nats() -> a__adx(a__zeros())
a__zeros() -> cons(0(),zeros())
a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
a__hd(cons(X,Y)) -> mark(X)
a__tl(cons(X,Y)) -> mark(Y)
mark(nats()) -> a__nats()
mark(adx(X)) -> a__adx(mark(X))
mark(zeros()) -> a__zeros()
mark(incr(X)) -> a__incr(mark(X))
mark(hd(X)) -> a__hd(mark(X))
mark(tl(X)) -> a__tl(mark(X))
mark(cons(X1,X2)) -> cons(X1,X2)
mark(0()) -> 0()
mark(s(X)) -> s(X)
a__nats() -> nats()
a__adx(X) -> adx(X)
a__zeros() -> zeros()
a__incr(X) -> incr(X)
a__hd(X) -> hd(X)
a__tl(X) -> tl(X)

Proof:
Complexity Transformation Processor:
  strict:
   a__nats() -> a__adx(a__zeros())
   a__zeros() -> cons(0(),zeros())
   a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
   a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
   a__hd(cons(X,Y)) -> mark(X)
   a__tl(cons(X,Y)) -> mark(Y)
   mark(nats()) -> a__nats()
   mark(adx(X)) -> a__adx(mark(X))
   mark(zeros()) -> a__zeros()
   mark(incr(X)) -> a__incr(mark(X))
   mark(hd(X)) -> a__hd(mark(X))
   mark(tl(X)) -> a__tl(mark(X))
   mark(cons(X1,X2)) -> cons(X1,X2)
   mark(0()) -> 0()
   mark(s(X)) -> s(X)
   a__nats() -> nats()
   a__adx(X) -> adx(X)
   a__zeros() -> zeros()
   a__incr(X) -> incr(X)
   a__hd(X) -> hd(X)
   a__tl(X) -> tl(X)
  weak:

  Matrix Interpretation Processor:
   dimension: 3
   max_matrix:
    [1 6 3]
    [0 1 4]
    [0 0 1]
    interpretation:
                [1 2 1]     [3]
     [tl](x0) = [0 1 4]x0 + [2]
                [0 0 1]     [1],

                [1 0 3]     [0]
     [hd](x0) = [0 1 1]x0 + [5]
                [0 0 1]     [1],

              [2]
     [nats] = [1]
              [3],

                   [1 2 1]     [4]
     [a__tl](x0) = [0 1 4]x0 + [2]
                   [0 0 1]     [1],

                  [1 1 1]     [1]
     [mark](x0) = [0 1 2]x0 + [0]
                  [0 0 1]     [0],

                   [1 0 3]     [5]
     [a__hd](x0) = [0 1 1]x0 + [6]
                   [0 0 1]     [1],

                 [1 0 0]     [2]
     [adx](x0) = [0 1 4]x0 + [0]
                 [0 0 1]     [3],

                       [0]
     [incr](x0) = x0 + [4]
                       [0],

               [1 1 0]
     [s](x0) = [0 0 0]x0
               [0 0 0]  ,

                          [1]
     [a__incr](x0) = x0 + [4]
                          [0],

                      [1 6 1]
     [cons](x0, x1) = [0 1 1]x0 + x1
                      [0 0 1]       ,

               [0]
     [zeros] = [2]
               [0],

           [0]
     [0] = [0]
           [0],

                    [1 0 1]     [4]
     [a__adx](x0) = [0 1 4]x0 + [4]
                    [0 0 1]     [3],

                  [1]
     [a__zeros] = [2]
                  [0],

                 [6]
     [a__nats] = [7]
                 [3]
    orientation:
                 [6]    [5]
     a__nats() = [7] >= [6] = a__adx(a__zeros())
                 [3]    [3]

                  [1]    [0]
     a__zeros() = [2] >= [2] = cons(0(),zeros())
                  [0]    [0]

                          [1 6 1]        [1]    [1 1 0]        [0]
     a__incr(cons(X,Y)) = [0 1 1]X + Y + [4] >= [0 0 0]X + Y + [4] = cons(s(X),incr(Y))
                          [0 0 1]        [0]    [0 0 0]        [0]

                         [1 6 2]    [1 0 1]    [4]    [1 6 1]    [1 0 0]    [3]
     a__adx(cons(X,Y)) = [0 1 5]X + [0 1 4]Y + [4] >= [0 1 1]X + [0 1 4]Y + [4] = a__incr(cons(X,adx(Y)))
                         [0 0 1]    [0 0 1]    [3]    [0 0 1]    [0 0 1]    [3]

                        [1 6 4]    [1 0 3]    [5]    [1 1 1]    [1]
     a__hd(cons(X,Y)) = [0 1 2]X + [0 1 1]Y + [6] >= [0 1 2]X + [0] = mark(X)
                        [0 0 1]    [0 0 1]    [1]    [0 0 1]    [0]

                        [1 8 4]    [1 2 1]    [4]    [1 1 1]    [1]
     a__tl(cons(X,Y)) = [0 1 5]X + [0 1 4]Y + [2] >= [0 1 2]Y + [0] = mark(Y)
                        [0 0 1]    [0 0 1]    [1]    [0 0 1]    [0]

                    [7]    [6]
     mark(nats()) = [7] >= [7] = a__nats()
                    [3]    [3]

                    [1 1 5]    [6]    [1 1 2]    [5]
     mark(adx(X)) = [0 1 6]X + [6] >= [0 1 6]X + [4] = a__adx(mark(X))
                    [0 0 1]    [3]    [0 0 1]    [3]

                     [3]    [1]
     mark(zeros()) = [2] >= [2] = a__zeros()
                     [0]    [0]

                     [1 1 1]    [5]    [1 1 1]    [2]
     mark(incr(X)) = [0 1 2]X + [4] >= [0 1 2]X + [4] = a__incr(mark(X))
                     [0 0 1]    [0]    [0 0 1]    [0]

                   [1 1 5]    [7]    [1 1 4]    [6]
     mark(hd(X)) = [0 1 3]X + [7] >= [0 1 3]X + [6] = a__hd(mark(X))
                   [0 0 1]    [1]    [0 0 1]    [1]

                   [1 3 6]    [7]    [1 3 6]    [5]
     mark(tl(X)) = [0 1 6]X + [4] >= [0 1 6]X + [2] = a__tl(mark(X))
                   [0 0 1]    [1]    [0 0 1]    [1]

                         [1 7 3]     [1 1 1]     [1]    [1 6 1]
     mark(cons(X1,X2)) = [0 1 3]X1 + [0 1 2]X2 + [0] >= [0 1 1]X1 + X2 = cons(X1,X2)
                         [0 0 1]     [0 0 1]     [0]    [0 0 1]

                 [1]    [0]
     mark(0()) = [0] >= [0] = 0()
                 [0]    [0]

                  [1 1 0]    [1]    [1 1 0]
     mark(s(X)) = [0 0 0]X + [0] >= [0 0 0]X = s(X)
                  [0 0 0]    [0]    [0 0 0]

                 [6]    [2]
     a__nats() = [7] >= [1] = nats()
                 [3]    [3]

                 [1 0 1]    [4]    [1 0 0]    [2]
     a__adx(X) = [0 1 4]X + [4] >= [0 1 4]X + [0] = adx(X)
                 [0 0 1]    [3]    [0 0 1]    [3]

                  [1]    [0]
     a__zeros() = [2] >= [2] = zeros()
                  [0]    [0]

                      [1]        [0]
     a__incr(X) = X + [4] >= X + [4] = incr(X)
                      [0]        [0]

                [1 0 3]    [5]    [1 0 3]    [0]
     a__hd(X) = [0 1 1]X + [6] >= [0 1 1]X + [5] = hd(X)
                [0 0 1]    [1]    [0 0 1]    [1]

                [1 2 1]    [4]    [1 2 1]    [3]
     a__tl(X) = [0 1 4]X + [2] >= [0 1 4]X + [2] = tl(X)
                [0 0 1]    [1]    [0 0 1]    [1]
    problem:
     strict:

     weak:
      a__nats() -> a__adx(a__zeros())
      a__zeros() -> cons(0(),zeros())
      a__incr(cons(X,Y)) -> cons(s(X),incr(Y))
      a__adx(cons(X,Y)) -> a__incr(cons(X,adx(Y)))
      a__hd(cons(X,Y)) -> mark(X)
      a__tl(cons(X,Y)) -> mark(Y)
      mark(nats()) -> a__nats()
      mark(adx(X)) -> a__adx(mark(X))
      mark(zeros()) -> a__zeros()
      mark(incr(X)) -> a__incr(mark(X))
      mark(hd(X)) -> a__hd(mark(X))
      mark(tl(X)) -> a__tl(mark(X))
      mark(cons(X1,X2)) -> cons(X1,X2)
      mark(0()) -> 0()
      mark(s(X)) -> s(X)
      a__nats() -> nats()
      a__adx(X) -> adx(X)
      a__zeros() -> zeros()
      a__incr(X) -> incr(X)
      a__hd(X) -> hd(X)
      a__tl(X) -> tl(X)
    Qed

Tool IRC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 ExIntrod GM04 GM

stdout:

MAYBE

Tool IRC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 ExIntrod GM04 GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    innermost runtime-complexity with respect to
  Rules:
    {  a__nats() -> a__adx(a__zeros())
     , a__zeros() -> cons(0(), zeros())
     , a__incr(cons(X, Y)) -> cons(s(X), incr(Y))
     , a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y)))
     , a__hd(cons(X, Y)) -> mark(X)
     , a__tl(cons(X, Y)) -> mark(Y)
     , mark(nats()) -> a__nats()
     , mark(adx(X)) -> a__adx(mark(X))
     , mark(zeros()) -> a__zeros()
     , mark(incr(X)) -> a__incr(mark(X))
     , mark(hd(X)) -> a__hd(mark(X))
     , mark(tl(X)) -> a__tl(mark(X))
     , mark(cons(X1, X2)) -> cons(X1, X2)
     , mark(0()) -> 0()
     , mark(s(X)) -> s(X)
     , a__nats() -> nats()
     , a__adx(X) -> adx(X)
     , a__zeros() -> zeros()
     , a__incr(X) -> incr(X)
     , a__hd(X) -> hd(X)
     , a__tl(X) -> tl(X)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds

Tool RC1

Execution Time	Unknown
Answer	MAYBE
Input	Transformed CSR 04 ExIntrod GM04 GM

stdout:

MAYBE

Tool RC2

Execution Time	Unknown
Answer	TIMEOUT
Input	Transformed CSR 04 ExIntrod GM04 GM

stdout:

TIMEOUT

'Fastest (timeout of 60.0 seconds)'
-----------------------------------
Answer:           TIMEOUT
Input Problem:    runtime-complexity with respect to
  Rules:
    {  a__nats() -> a__adx(a__zeros())
     , a__zeros() -> cons(0(), zeros())
     , a__incr(cons(X, Y)) -> cons(s(X), incr(Y))
     , a__adx(cons(X, Y)) -> a__incr(cons(X, adx(Y)))
     , a__hd(cons(X, Y)) -> mark(X)
     , a__tl(cons(X, Y)) -> mark(Y)
     , mark(nats()) -> a__nats()
     , mark(adx(X)) -> a__adx(mark(X))
     , mark(zeros()) -> a__zeros()
     , mark(incr(X)) -> a__incr(mark(X))
     , mark(hd(X)) -> a__hd(mark(X))
     , mark(tl(X)) -> a__tl(mark(X))
     , mark(cons(X1, X2)) -> cons(X1, X2)
     , mark(0()) -> 0()
     , mark(s(X)) -> s(X)
     , a__nats() -> nats()
     , a__adx(X) -> adx(X)
     , a__zeros() -> zeros()
     , a__incr(X) -> incr(X)
     , a__hd(X) -> hd(X)
     , a__tl(X) -> tl(X)}

Proof Output:
  Computation stopped due to timeout after 60.0 seconds