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.55
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳6 CdtProblem0.00/0.55
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID))0.00/0.55
↳8 BOUNDS(O(1), O(1))0.00/0.55
zeros → cons(0, n__zeros) 0.00/0.55
tail(cons(X, XS)) → activate(XS) 0.00/0.55
zeros → n__zeros 0.00/0.55
activate(n__zeros) → zeros 0.00/0.55
activate(X) → X
Tuples:
zeros → cons(0, n__zeros) 0.00/0.55
zeros → n__zeros 0.00/0.55
tail(cons(z0, z1)) → activate(z1) 0.00/0.55
activate(n__zeros) → zeros 0.00/0.55
activate(z0) → z0
S tuples:
TAIL(cons(z0, z1)) → c2(ACTIVATE(z1)) 0.00/0.55
ACTIVATE(n__zeros) → c3(ZEROS)
K tuples:none
TAIL(cons(z0, z1)) → c2(ACTIVATE(z1)) 0.00/0.55
ACTIVATE(n__zeros) → c3(ZEROS)
zeros, tail, activate
TAIL, ACTIVATE
c2, c3
Tuples:
zeros → cons(0, n__zeros) 0.00/0.55
zeros → n__zeros 0.00/0.55
tail(cons(z0, z1)) → activate(z1) 0.00/0.55
activate(n__zeros) → zeros 0.00/0.55
activate(z0) → z0
S tuples:
TAIL(cons(z0, z1)) → c2(ACTIVATE(z1)) 0.00/0.55
ACTIVATE(n__zeros) → c3
K tuples:none
TAIL(cons(z0, z1)) → c2(ACTIVATE(z1)) 0.00/0.55
ACTIVATE(n__zeros) → c3
zeros, tail, activate
TAIL, ACTIVATE
c2, c3
ACTIVATE(n__zeros) → c3 0.00/0.55
TAIL(cons(z0, z1)) → c2(ACTIVATE(z1))
Tuples:none
zeros → cons(0, n__zeros) 0.00/0.55
zeros → n__zeros 0.00/0.55
tail(cons(z0, z1)) → activate(z1) 0.00/0.55
activate(n__zeros) → zeros 0.00/0.55
activate(z0) → z0
zeros, tail, activate