YES(O(1), O(n^1)) 0.00/0.79 YES(O(1), O(n^1)) 0.00/0.81 0.00/0.81 0.00/0.81
0.00/0.81 0.00/0.810 CpxTRS0.00/0.81
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.81
↳2 CdtProblem0.00/0.81
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.81
↳4 CdtProblem0.00/0.81
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.81
↳6 CdtProblem0.00/0.81
↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.81
↳8 CdtProblem0.00/0.81
↳9 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))))0.00/0.81
↳10 CdtProblem0.00/0.81
↳11 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.81
↳12 BOUNDS(O(1), O(1))0.00/0.81
first(0, X) → nil 0.00/0.81
first(s(X), cons(Y, Z)) → cons(Y, n__first(X, activate(Z))) 0.00/0.81
from(X) → cons(X, n__from(s(X))) 0.00/0.81
first(X1, X2) → n__first(X1, X2) 0.00/0.81
from(X) → n__from(X) 0.00/0.81
activate(n__first(X1, X2)) → first(X1, X2) 0.00/0.81
activate(n__from(X)) → from(X) 0.00/0.81
activate(X) → X
Tuples:
first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
S tuples:
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6(FROM(z0))
K tuples:none
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6(FROM(z0))
first, from, activate
FIRST, ACTIVATE
c1, c5, c6
Tuples:
first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
S tuples:
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
K tuples:none
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
first, from, activate
FIRST, ACTIVATE
c1, c5, c6
ACTIVATE(n__from(z0)) → c6
Tuples:
first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
S tuples:
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
K tuples:none
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
first, from, activate
FIRST, ACTIVATE
c1, c5, c6
We considered the (Usable) Rules:none
ACTIVATE(n__from(z0)) → c6
The order we found is given by the following interpretation:
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
POL(ACTIVATE(x1)) = [2] 0.00/0.81
POL(FIRST(x1, x2)) = [2] 0.00/0.81
POL(c1(x1)) = x1 0.00/0.81
POL(c5(x1)) = x1 0.00/0.81
POL(c6) = 0 0.00/0.81
POL(cons(x1, x2)) = 0 0.00/0.81
POL(n__first(x1, x2)) = 0 0.00/0.81
POL(n__from(x1)) = 0 0.00/0.81
POL(s(x1)) = 0
Tuples:
first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
S tuples:
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
K tuples:
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1))
Defined Rule Symbols:
ACTIVATE(n__from(z0)) → c6
first, from, activate
FIRST, ACTIVATE
c1, c5, c6
We considered the (Usable) Rules:none
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1))
The order we found is given by the following interpretation:
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
POL(ACTIVATE(x1)) = [2] + [4]x1 0.00/0.81
POL(FIRST(x1, x2)) = [4]x2 0.00/0.81
POL(c1(x1)) = x1 0.00/0.81
POL(c5(x1)) = x1 0.00/0.81
POL(c6) = 0 0.00/0.81
POL(cons(x1, x2)) = [1] + x2 0.00/0.81
POL(n__first(x1, x2)) = [1] + x2 0.00/0.81
POL(n__from(x1)) = 0 0.00/0.81
POL(s(x1)) = [1]
Tuples:
first(0, z0) → nil 0.00/0.81
first(s(z0), cons(z1, z2)) → cons(z1, n__first(z0, activate(z2))) 0.00/0.81
first(z0, z1) → n__first(z0, z1) 0.00/0.81
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.81
from(z0) → n__from(z0) 0.00/0.81
activate(n__first(z0, z1)) → first(z0, z1) 0.00/0.81
activate(n__from(z0)) → from(z0) 0.00/0.81
activate(z0) → z0
S tuples:none
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1)) 0.00/0.81
ACTIVATE(n__from(z0)) → c6
Defined Rule Symbols:
ACTIVATE(n__from(z0)) → c6 0.00/0.81
FIRST(s(z0), cons(z1, z2)) → c1(ACTIVATE(z2)) 0.00/0.81
ACTIVATE(n__first(z0, z1)) → c5(FIRST(z0, z1))
first, from, activate
FIRST, ACTIVATE
c1, c5, c6