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) |
length(nil) | → | 0 | (4) |
length(cons(N,L)) | → | U11(tt,activate(L)) | (5) |
zeros | → | n__zeros | (6) |
activate(n__zeros) | → | zeros | (7) |
activate(X) | → | X | (8) |
t0 | = | U11(tt,n__zeros) |
→ | U12(tt,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(U11(tt,n__zeros)) | |
= | t7 |