Problem Transformed CSR 04 Ex3 3 25 Bor03 L

Tool Bounds

Execution Time	4.161191e-2ms
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex3 3 25 Bor03 L

stdout:

YES(?,O(n^1))

We consider the following Problem:

  Strict Trs:
    {  prefix(L) -> cons(nil())
     , zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))
     , zWadr(XS, nil()) -> nil()
     , zWadr(nil(), YS) -> nil()
     , from(X) -> cons(X)
     , app(cons(X), YS) -> cons(X)
     , app(nil(), YS) -> YS}
  StartTerms: all
  Strategy: none

Certificate: YES(?,O(n^1))

Proof:
  The problem is match-bounded by 2.
  The enriched problem is compatible with the following automaton:
  {  nil_0() -> 1
   , nil_0() -> 2
   , nil_1() -> 1
   , nil_1() -> 2
   , app_0(1, 1) -> 1
   , app_0(1, 1) -> 2
   , app_1(1, 1) -> 2
   , app_1(1, 3) -> 2
   , app_1(2, 1) -> 2
   , app_1(2, 3) -> 2
   , cons_0(1) -> 1
   , cons_0(1) -> 2
   , cons_1(1) -> 1
   , cons_1(1) -> 2
   , cons_1(1) -> 3
   , cons_1(2) -> 1
   , cons_1(2) -> 2
   , cons_2(1) -> 2
   , cons_2(2) -> 2
   , from_0(1) -> 1
   , from_0(1) -> 2
   , zWadr_0(1, 1) -> 1
   , zWadr_0(1, 1) -> 2
   , prefix_0(1) -> 1
   , prefix_0(1) -> 2}

Hurray, we answered YES(?,O(n^1))

Tool CDI

Execution Time	2.246348ms
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 Ex3 3 25 Bor03 L

stdout:

YES(?,O(n^2))
QUADRATIC upper bound on the derivational complexity

This TRS is terminating using the deltarestricted interpretation
prefix(delta, X0) =  + 0*X0 + 0 + 1*X0*delta + 1*delta
zWadr(delta, X1, X0) =  + 1*X0 + 1*X1 + 0 + 0*X0*delta + 0*X1*delta + 2*delta
from(delta, X0) =  + 1*X0 + 0 + 0*X0*delta + 2*delta
cons(delta, X0) =  + 1*X0 + 0 + 0*X0*delta + 0*delta
nil(delta) =  + 0 + 0*delta
app(delta, X1, X0) =  + 1*X0 + 1*X1 + 0 + 0*X0*delta + 0*X1*delta + 1*delta
prefix_tau_1(delta) = delta/(0 + 1 * delta)
zWadr_tau_1(delta) = delta/(1 + 0 * delta)
zWadr_tau_2(delta) = delta/(1 + 0 * delta)
from_tau_1(delta) = delta/(1 + 0 * delta)
cons_tau_1(delta) = delta/(1 + 0 * delta)
app_tau_1(delta) = delta/(1 + 0 * delta)
app_tau_2(delta) = delta/(1 + 0 * delta)

Time: 2.207699 seconds
Statistics:
Number of monomials: 525
Last formula building started for bound 3
Last SAT solving started for bound 3

Tool EDA

Execution Time	0.14679193ms
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex3 3 25 Bor03 L

stdout:

Tool IDA

Execution Time	0.3178482ms
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex3 3 25 Bor03 L

stdout:

Tool TRI

Execution Time	8.352399e-2ms
Answer	YES(?,O(n^1))
Input	Transformed CSR 04 Ex3 3 25 Bor03 L

stdout:

Tool TRI2

Execution Time	0.17230201ms
Answer	YES(?,O(n^2))
Input	Transformed CSR 04 Ex3 3 25 Bor03 L

stdout:

YES(?,O(n^2))

We consider the following Problem:

  Strict Trs:
    {  prefix(L) -> cons(nil())
     , zWadr(cons(X), cons(Y)) -> cons(app(Y, cons(X)))
     , zWadr(XS, nil()) -> nil()
     , zWadr(nil(), YS) -> nil()
     , from(X) -> cons(X)
     , app(cons(X), YS) -> cons(X)
     , app(nil(), YS) -> YS}
  StartTerms: all
  Strategy: none

Certificate: YES(?,O(n^2))

Proof:
  We have the following triangular matrix interpretation:
  Interpretation Functions:
   nil() = [0]
           [1]
   app(x1, x2) = [1 1] x1 + [1 0] x2 + [0]
                 [0 0]      [0 1]      [2]
   cons(x1) = [1 1] x1 + [1]
              [0 0]      [1]
   from(x1) = [1 3] x1 + [3]
              [0 1]      [3]
   zWadr(x1, x2) = [1 3] x1 + [1 0] x2 + [3]
                   [0 0]      [0 0]      [1]
   prefix(x1) = [1 0] x1 + [3]
                [0 0]      [3]

Hurray, we answered YES(?,O(n^2))