The rewrite relation of the following TRS is considered.
from(X) | → | cons(X,n__from(s(X))) | (1) |
length(n__nil) | → | 0 | (2) |
length(n__cons(X,Y)) | → | s(length1(activate(Y))) | (3) |
length1(X) | → | length(activate(X)) | (4) |
from(X) | → | n__from(X) | (5) |
nil | → | n__nil | (6) |
cons(X1,X2) | → | n__cons(X1,X2) | (7) |
activate(n__from(X)) | → | from(X) | (8) |
activate(n__nil) | → | nil | (9) |
activate(n__cons(X1,X2)) | → | cons(X1,X2) | (10) |
activate(X) | → | X | (11) |
t0 | = | length(n__cons(X,n__from(x42749))) |
→ | s(length1(activate(n__from(x42749)))) | |
→ | s(length(activate(activate(n__from(x42749))))) | |
→ | s(length(activate(n__from(x42749)))) | |
→ | s(length(from(x42749))) | |
→ | s(length(cons(x42749,n__from(s(x42749))))) | |
→ | s(length(n__cons(x42749,n__from(s(x42749))))) | |
= | t6 |