The rewrite relation of the following TRS is considered.
zeros | → | cons(0,n__zeros) | (1) |
U11(tt,L) | → | U12(tt,activate(L)) | (2) |
U12(tt,L) | → | s(length(activate(L))) | (3) |
U21(tt,IL,M,N) | → | U22(tt,activate(IL),activate(M),activate(N)) | (4) |
U22(tt,IL,M,N) | → | U23(tt,activate(IL),activate(M),activate(N)) | (5) |
U23(tt,IL,M,N) | → | cons(activate(N),n__take(activate(M),activate(IL))) | (6) |
length(nil) | → | 0 | (7) |
length(cons(N,L)) | → | U11(tt,activate(L)) | (8) |
take(0,IL) | → | nil | (9) |
take(s(M),cons(N,IL)) | → | U21(tt,activate(IL),M,N) | (10) |
zeros | → | n__zeros | (11) |
take(X1,X2) | → | n__take(X1,X2) | (12) |
activate(n__zeros) | → | zeros | (13) |
activate(n__take(X1,X2)) | → | take(activate(X1),activate(X2)) | (14) |
activate(X) | → | X | (15) |
t0 | = | U12(tt,activate(activate(n__zeros))) |
→ | s(length(activate(activate(activate(n__zeros))))) | |
→ | s(length(activate(activate(n__zeros)))) | |
→ | s(length(activate(n__zeros))) | |
→ | s(length(zeros)) | |
→ | s(length(cons(0,n__zeros))) | |
→ | s(U11(tt,activate(n__zeros))) | |
→ | s(U12(tt,activate(activate(n__zeros)))) | |
= | t7 |