YES(O(1), O(1)) 0.00/0.54 YES(O(1), O(1)) 0.00/0.55 0.00/0.55 0.00/0.55
0.00/0.55 0.00/0.550 CpxTRS0.00/0.55
↳1 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳2 CdtProblem0.00/0.55
↳3 CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳4 CdtProblem0.00/0.56
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳6 CdtProblem0.00/0.56
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.56
↳8 BOUNDS(O(1), O(1))0.00/0.56
2nd(cons1(X, cons(Y, Z))) → Y 0.00/0.56
2nd(cons(X, X1)) → 2nd(cons1(X, activate(X1))) 0.00/0.56
from(X) → cons(X, n__from(s(X))) 0.00/0.56
from(X) → n__from(X) 0.00/0.56
activate(n__from(X)) → from(X) 0.00/0.56
activate(X) → X
Tuples:
2nd(cons1(z0, cons(z1, z2))) → z1 0.00/0.56
2nd(cons(z0, z1)) → 2nd(cons1(z0, 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
activate(n__from(z0)) → from(z0) 0.00/0.56
activate(z0) → z0
S tuples:
2ND(cons(z0, z1)) → c1(2ND(cons1(z0, activate(z1))), ACTIVATE(z1)) 0.00/0.56
ACTIVATE(n__from(z0)) → c4(FROM(z0))
K tuples:none
2ND(cons(z0, z1)) → c1(2ND(cons1(z0, activate(z1))), ACTIVATE(z1)) 0.00/0.56
ACTIVATE(n__from(z0)) → c4(FROM(z0))
2nd, from, activate
2ND, ACTIVATE
c1, c4
Tuples:
2nd(cons1(z0, cons(z1, z2))) → z1 0.00/0.56
2nd(cons(z0, z1)) → 2nd(cons1(z0, 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
activate(n__from(z0)) → from(z0) 0.00/0.56
activate(z0) → z0
S tuples:
2ND(cons(z0, z1)) → c1(ACTIVATE(z1)) 0.00/0.56
ACTIVATE(n__from(z0)) → c4
K tuples:none
2ND(cons(z0, z1)) → c1(ACTIVATE(z1)) 0.00/0.56
ACTIVATE(n__from(z0)) → c4
2nd, from, activate
2ND, ACTIVATE
c1, c4
2ND(cons(z0, z1)) → c1(ACTIVATE(z1)) 0.00/0.56
ACTIVATE(n__from(z0)) → c4
Tuples:none
2nd(cons1(z0, cons(z1, z2))) → z1 0.00/0.56
2nd(cons(z0, z1)) → 2nd(cons1(z0, 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
activate(n__from(z0)) → from(z0) 0.00/0.56
activate(z0) → z0
2nd, from, activate