YES(O(1), O(n^2)) 0.00/0.85 YES(O(1), O(n^2)) 0.00/0.87 0.00/0.87 0.00/0.87
0.00/0.87 0.00/0.870 CpxTRS0.00/0.87
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.87
↳2 CdtProblem0.00/0.87
↳3 CdtUnreachableProof (⇔)0.00/0.87
↳4 CdtProblem0.00/0.87
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.87
↳6 CdtProblem0.00/0.87
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.87
↳8 CdtProblem0.00/0.87
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.87
↳10 CdtProblem0.00/0.87
↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))))0.00/0.87
↳12 CdtProblem0.00/0.87
↳13 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.87
↳14 BOUNDS(O(1), O(1))0.00/0.87
f(cons(nil, y)) → y 0.00/0.87
f(cons(f(cons(nil, y)), z)) → copy(n, y, z) 0.00/0.87
copy(0, y, z) → f(z) 0.00/0.87
copy(s(x), y, z) → copy(x, y, cons(f(y), z))
Tuples:
f(cons(nil, z0)) → z0 0.00/0.87
f(cons(f(cons(nil, z0)), z1)) → copy(n, z0, z1) 0.00/0.87
copy(0, z0, z1) → f(z1) 0.00/0.87
copy(s(z0), z1, z2) → copy(z0, z1, cons(f(z1), z2))
S tuples:
F(cons(f(cons(nil, z0)), z1)) → c1(COPY(n, z0, z1)) 0.00/0.87
COPY(0, z0, z1) → c2(F(z1)) 0.00/0.87
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)), F(z1))
K tuples:none
F(cons(f(cons(nil, z0)), z1)) → c1(COPY(n, z0, z1)) 0.00/0.87
COPY(0, z0, z1) → c2(F(z1)) 0.00/0.87
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)), F(z1))
f, copy
F, COPY
c1, c2, c3
F(cons(f(cons(nil, z0)), z1)) → c1(COPY(n, z0, z1))
Tuples:
f(cons(nil, z0)) → z0 0.00/0.88
f(cons(f(cons(nil, z0)), z1)) → copy(n, z0, z1) 0.00/0.88
copy(0, z0, z1) → f(z1) 0.00/0.88
copy(s(z0), z1, z2) → copy(z0, z1, cons(f(z1), z2))
S tuples:
COPY(0, z0, z1) → c2(F(z1)) 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)), F(z1))
K tuples:none
COPY(0, z0, z1) → c2(F(z1)) 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)), F(z1))
f, copy
COPY
c2, c3
Tuples:
f(cons(nil, z0)) → z0 0.00/0.88
f(cons(f(cons(nil, z0)), z1)) → copy(n, z0, z1) 0.00/0.88
copy(0, z0, z1) → f(z1) 0.00/0.88
copy(s(z0), z1, z2) → copy(z0, z1, cons(f(z1), z2))
S tuples:
COPY(0, z0, z1) → c2 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
K tuples:none
COPY(0, z0, z1) → c2 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
f, copy
COPY
c2, c3
COPY(0, z0, z1) → c2
Tuples:
f(cons(nil, z0)) → z0 0.00/0.88
f(cons(f(cons(nil, z0)), z1)) → copy(n, z0, z1) 0.00/0.88
copy(0, z0, z1) → f(z1) 0.00/0.88
copy(s(z0), z1, z2) → copy(z0, z1, cons(f(z1), z2))
S tuples:
COPY(0, z0, z1) → c2 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
K tuples:none
COPY(0, z0, z1) → c2 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
f, copy
COPY
c2, c3
We considered the (Usable) Rules:
COPY(0, z0, z1) → c2
And the Tuples:
f(cons(nil, z0)) → z0
The order we found is given by the following interpretation:
COPY(0, z0, z1) → c2 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
POL(0) = [3] 0.00/0.88
POL(COPY(x1, x2, x3)) = [5] 0.00/0.88
POL(c2) = 0 0.00/0.88
POL(c3(x1)) = x1 0.00/0.88
POL(cons(x1, x2)) = [1] + x2 0.00/0.88
POL(f(x1)) = [1] 0.00/0.88
POL(nil) = 0 0.00/0.88
POL(s(x1)) = [1] + x1
Tuples:
f(cons(nil, z0)) → z0 0.00/0.88
f(cons(f(cons(nil, z0)), z1)) → copy(n, z0, z1) 0.00/0.88
copy(0, z0, z1) → f(z1) 0.00/0.88
copy(s(z0), z1, z2) → copy(z0, z1, cons(f(z1), z2))
S tuples:
COPY(0, z0, z1) → c2 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
K tuples:
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
Defined Rule Symbols:
COPY(0, z0, z1) → c2
f, copy
COPY
c2, c3
We considered the (Usable) Rules:
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
And the Tuples:
f(cons(nil, z0)) → z0
The order we found is given by the following interpretation:
COPY(0, z0, z1) → c2 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
POL(0) = 0 0.00/0.88
POL(COPY(x1, x2, x3)) = [2]x3 + x12 0.00/0.88
POL(c2) = 0 0.00/0.88
POL(c3(x1)) = x1 0.00/0.88
POL(cons(x1, x2)) = 0 0.00/0.88
POL(f(x1)) = [3]x1 0.00/0.88
POL(nil) = [3] 0.00/0.88
POL(s(x1)) = [2] + x1
Tuples:
f(cons(nil, z0)) → z0 0.00/0.88
f(cons(f(cons(nil, z0)), z1)) → copy(n, z0, z1) 0.00/0.88
copy(0, z0, z1) → f(z1) 0.00/0.88
copy(s(z0), z1, z2) → copy(z0, z1, cons(f(z1), z2))
S tuples:none
COPY(0, z0, z1) → c2 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
Defined Rule Symbols:
COPY(0, z0, z1) → c2 0.00/0.88
COPY(s(z0), z1, z2) → c3(COPY(z0, z1, cons(f(z1), z2)))
f, copy
COPY
c2, c3