The rewrite relation of the following TRS is considered.
from(X) | → | cons(X,n__from(n__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) |
s(X) | → | n__s(X) | (6) |
nil | → | n__nil | (7) |
cons(X1,X2) | → | n__cons(X1,X2) | (8) |
activate(n__from(X)) | → | from(activate(X)) | (9) |
activate(n__s(X)) | → | s(activate(X)) | (10) |
activate(n__nil) | → | nil | (11) |
activate(n__cons(X1,X2)) | → | cons(activate(X1),X2) | (12) |
activate(X) | → | X | (13) |
from#(X) | → | cons#(X,n__from(n__s(X))) | (14) |
length#(n__cons(X,Y)) | → | s#(length1(activate(Y))) | (15) |
length#(n__cons(X,Y)) | → | length1#(activate(Y)) | (16) |
length#(n__cons(X,Y)) | → | activate#(Y) | (17) |
length1#(X) | → | length#(activate(X)) | (18) |
length1#(X) | → | activate#(X) | (19) |
activate#(n__from(X)) | → | from#(activate(X)) | (20) |
activate#(n__from(X)) | → | activate#(X) | (21) |
activate#(n__s(X)) | → | s#(activate(X)) | (22) |
activate#(n__s(X)) | → | activate#(X) | (23) |
activate#(n__nil) | → | nil# | (24) |
activate#(n__cons(X1,X2)) | → | cons#(activate(X1),X2) | (25) |
activate#(n__cons(X1,X2)) | → | activate#(X1) | (26) |
from#(X) | → | cons#(X,n__from(n__s(X))) | (14) |
length#(n__cons(X,Y)) | → | s#(length1(activate(Y))) | (15) |
length#(n__cons(X,Y)) | → | activate#(Y) | (17) |
length1#(X) | → | activate#(X) | (19) |
activate#(n__from(X)) | → | from#(activate(X)) | (20) |
activate#(n__from(X)) | → | activate#(X) | (21) |
activate#(n__s(X)) | → | s#(activate(X)) | (22) |
activate#(n__s(X)) | → | activate#(X) | (23) |
activate#(n__nil) | → | nil# | (24) |
activate#(n__cons(X1,X2)) | → | cons#(activate(X1),X2) | (25) |
activate#(n__cons(X1,X2)) | → | activate#(X1) | (26) |
length1#(n__from(x0)) | → | length#(from(activate(x0))) | (27) |
length1#(n__s(x0)) | → | length#(s(activate(x0))) | (28) |
length1#(n__nil) | → | length#(nil) | (29) |
length1#(n__cons(x0,x1)) | → | length#(cons(activate(x0),x1)) | (30) |
length1#(x0) | → | length#(x0) | (31) |
length1#(n__nil) | → | length#(n__nil) | (32) |
length1#(n__nil) | → | length#(n__nil) | (32) |
length1#(n__s(x0)) | → | length#(s(activate(x0))) | (28) |
t0 | = | length#(from(X)) |
→R | length#(cons(X,n__from(n__s(X)))) | |
→R | length#(n__cons(X,n__from(n__s(X)))) | |
→P | length1#(activate(n__from(n__s(X)))) | |
→R | length1#(n__from(n__s(X))) | |
→P | length#(from(activate(n__s(X)))) | |
= | t5 |