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) |
from#(X) | → | cons#(X,n__from(s(X))) | (12) |
length#(n__cons(X,Y)) | → | length1#(activate(Y)) | (13) |
length#(n__cons(X,Y)) | → | activate#(Y) | (14) |
length1#(X) | → | length#(activate(X)) | (15) |
length1#(X) | → | activate#(X) | (16) |
activate#(n__from(X)) | → | from#(X) | (17) |
activate#(n__nil) | → | nil# | (18) |
activate#(n__cons(X1,X2)) | → | cons#(X1,X2) | (19) |
from#(X) | → | cons#(X,n__from(s(X))) | (12) |
length#(n__cons(X,Y)) | → | activate#(Y) | (14) |
length1#(X) | → | activate#(X) | (16) |
activate#(n__from(X)) | → | from#(X) | (17) |
activate#(n__nil) | → | nil# | (18) |
activate#(n__cons(X1,X2)) | → | cons#(X1,X2) | (19) |
length1#(n__from(x0)) | → | length#(from(x0)) | (20) |
length1#(n__nil) | → | length#(nil) | (21) |
length1#(n__cons(x0,x1)) | → | length#(cons(x0,x1)) | (22) |
length1#(x0) | → | length#(x0) | (23) |
length1#(n__from(x0)) | → | length#(cons(x0,n__from(s(x0)))) | (24) |
length1#(n__from(x0)) | → | length#(n__from(x0)) | (25) |
length1#(n__from(x0)) | → | length#(n__from(x0)) | (25) |
length1#(n__nil) | → | length#(n__nil) | (26) |
length1#(n__nil) | → | length#(n__nil) | (26) |
length1#(n__cons(x0,x1)) | → | length#(n__cons(x0,x1)) | (27) |
t0 | = | length1#(activate(n__from(x0))) |
→R | length1#(n__from(x0)) | |
→P | length#(cons(x0,n__from(s(x0)))) | |
→R | length#(n__cons(x0,n__from(s(x0)))) | |
→P | length1#(activate(n__from(s(x0)))) | |
= | t4 |