0 CpxTRS
↳1 RcToIrcProof (BOTH BOUNDS(ID, ID), 16 ms)
↳2 CpxTRS
↳3 CpxTrsToCdtProof (BOTH BOUNDS(ID, ID), 0 ms)
↳4 CdtProblem
↳5 CdtLeafRemovalProof (BOTH BOUNDS(ID, ID), 0 ms)
↳6 CdtProblem
↳7 SIsEmptyProof (BOTH BOUNDS(ID, ID), 0 ms)
↳8 BOUNDS(1, 1)
zeros → cons(0, n__zeros)
tail(cons(X, XS)) → activate(XS)
zeros → n__zeros
activate(n__zeros) → zeros
activate(X) → X
As the TRS does not nest defined symbols, we have rc = irc.
zeros → cons(0, n__zeros)
tail(cons(X, XS)) → activate(XS)
zeros → n__zeros
activate(n__zeros) → zeros
activate(X) → X
Tuples:
zeros → cons(0, n__zeros)
zeros → n__zeros
tail(cons(z0, z1)) → activate(z1)
activate(n__zeros) → zeros
activate(z0) → z0
S tuples:
ZEROS → c
ZEROS → c1
TAIL(cons(z0, z1)) → c2(ACTIVATE(z1))
ACTIVATE(n__zeros) → c3(ZEROS)
ACTIVATE(z0) → c4
K tuples:none
ZEROS → c
ZEROS → c1
TAIL(cons(z0, z1)) → c2(ACTIVATE(z1))
ACTIVATE(n__zeros) → c3(ZEROS)
ACTIVATE(z0) → c4
zeros, tail, activate
ZEROS, TAIL, ACTIVATE
c, c1, c2, c3, c4
TAIL(cons(z0, z1)) → c2(ACTIVATE(z1))
ACTIVATE(n__zeros) → c3(ZEROS)
ZEROS → c
ZEROS → c1
ACTIVATE(z0) → c4
Tuples:none
zeros → cons(0, n__zeros)
zeros → n__zeros
tail(cons(z0, z1)) → activate(z1)
activate(n__zeros) → zeros
activate(z0) → z0
zeros, tail, activate