YES(O(1), O(1)) 0.00/0.55 YES(O(1), O(1)) 0.00/0.56 0.00/0.56 0.00/0.56
0.00/0.56 0.00/0.560 CpxTRS0.00/0.56
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳2 CdtProblem0.00/0.56
↳3 CdtUnreachableProof (⇔)0.00/0.56
↳4 CdtProblem0.00/0.56
↳5 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳6 CdtProblem0.00/0.56
↳7 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳8 CdtProblem0.00/0.56
↳9 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳10 BOUNDS(O(1), O(1))0.00/0.56
2nd(cons(X, n__cons(Y, Z))) → activate(Y) 0.00/0.56
from(X) → cons(X, n__from(s(X))) 0.00/0.56
cons(X1, X2) → n__cons(X1, X2) 0.00/0.56
from(X) → n__from(X) 0.00/0.56
activate(n__cons(X1, X2)) → cons(X1, X2) 0.00/0.56
activate(n__from(X)) → from(X) 0.00/0.56
activate(X) → X
Tuples:
2nd(cons(z0, n__cons(z1, z2))) → activate(z1) 0.00/0.56
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.56
from(z0) → n__from(z0) 0.00/0.56
cons(z0, z1) → n__cons(z0, z1) 0.00/0.56
activate(n__cons(z0, z1)) → cons(z0, z1) 0.00/0.56
activate(n__from(z0)) → from(z0) 0.00/0.56
activate(z0) → z0
S tuples:
2ND(cons(z0, n__cons(z1, z2))) → c(ACTIVATE(z1)) 0.00/0.56
FROM(z0) → c1(CONS(z0, n__from(s(z0)))) 0.00/0.56
ACTIVATE(n__cons(z0, z1)) → c4(CONS(z0, z1)) 0.00/0.56
ACTIVATE(n__from(z0)) → c5(FROM(z0))
K tuples:none
2ND(cons(z0, n__cons(z1, z2))) → c(ACTIVATE(z1)) 0.00/0.56
FROM(z0) → c1(CONS(z0, n__from(s(z0)))) 0.00/0.56
ACTIVATE(n__cons(z0, z1)) → c4(CONS(z0, z1)) 0.00/0.56
ACTIVATE(n__from(z0)) → c5(FROM(z0))
2nd, from, cons, activate
2ND, FROM, ACTIVATE
c, c1, c4, c5
2ND(cons(z0, n__cons(z1, z2))) → c(ACTIVATE(z1))
Tuples:
2nd(cons(z0, n__cons(z1, z2))) → activate(z1) 0.00/0.56
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.56
from(z0) → n__from(z0) 0.00/0.56
cons(z0, z1) → n__cons(z0, z1) 0.00/0.56
activate(n__cons(z0, z1)) → cons(z0, z1) 0.00/0.56
activate(n__from(z0)) → from(z0) 0.00/0.56
activate(z0) → z0
S tuples:
FROM(z0) → c1(CONS(z0, n__from(s(z0)))) 0.00/0.56
ACTIVATE(n__cons(z0, z1)) → c4(CONS(z0, z1)) 0.00/0.56
ACTIVATE(n__from(z0)) → c5(FROM(z0))
K tuples:none
FROM(z0) → c1(CONS(z0, n__from(s(z0)))) 0.00/0.56
ACTIVATE(n__cons(z0, z1)) → c4(CONS(z0, z1)) 0.00/0.56
ACTIVATE(n__from(z0)) → c5(FROM(z0))
2nd, from, cons, activate
FROM, ACTIVATE
c1, c4, c5
Tuples:
2nd(cons(z0, n__cons(z1, z2))) → activate(z1) 0.00/0.56
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.56
from(z0) → n__from(z0) 0.00/0.56
cons(z0, z1) → n__cons(z0, z1) 0.00/0.56
activate(n__cons(z0, z1)) → cons(z0, z1) 0.00/0.56
activate(n__from(z0)) → from(z0) 0.00/0.56
activate(z0) → z0
S tuples:
ACTIVATE(n__from(z0)) → c5(FROM(z0)) 0.00/0.56
FROM(z0) → c1 0.00/0.56
ACTIVATE(n__cons(z0, z1)) → c4
K tuples:none
ACTIVATE(n__from(z0)) → c5(FROM(z0)) 0.00/0.56
FROM(z0) → c1 0.00/0.56
ACTIVATE(n__cons(z0, z1)) → c4
2nd, from, cons, activate
ACTIVATE, FROM
c5, c1, c4
ACTIVATE(n__from(z0)) → c5(FROM(z0)) 0.00/0.56
FROM(z0) → c1 0.00/0.56
ACTIVATE(n__cons(z0, z1)) → c4
Tuples:none
2nd(cons(z0, n__cons(z1, z2))) → activate(z1) 0.00/0.56
from(z0) → cons(z0, n__from(s(z0))) 0.00/0.56
from(z0) → n__from(z0) 0.00/0.56
cons(z0, z1) → n__cons(z0, z1) 0.00/0.56
activate(n__cons(z0, z1)) → cons(z0, z1) 0.00/0.56
activate(n__from(z0)) → from(z0) 0.00/0.56
activate(z0) → z0
2nd, from, cons, activate