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) |
length(nil) | → | 0 | (4) |
U11#(tt,L) | → | U12#(tt,activate(L)) | (9) |
U11#(tt,L) | → | activate#(L) | (10) |
U12#(tt,L) | → | length#(activate(L)) | (11) |
U12#(tt,L) | → | activate#(L) | (12) |
length#(cons(N,L)) | → | U11#(tt,activate(L)) | (13) |
length#(cons(N,L)) | → | activate#(L) | (14) |
activate#(n__zeros) | → | zeros# | (15) |
U11#(tt,L) | → | activate#(L) | (10) |
U12#(tt,L) | → | activate#(L) | (12) |
length#(cons(N,L)) | → | activate#(L) | (14) |
activate#(n__zeros) | → | zeros# | (15) |
U11(tt,L) | → | U12(tt,activate(L)) | (2) |
U12(tt,L) | → | s(length(activate(L))) | (3) |
length(cons(N,L)) | → | U11(tt,activate(L)) | (5) |
U12#(tt,n__zeros) | → | length#(zeros) | (16) |
U12#(tt,x0) | → | length#(x0) | (17) |
U12#(tt,n__zeros) | → | length#(cons(0,n__zeros)) | (18) |
U12#(tt,n__zeros) | → | length#(n__zeros) | (19) |
U12#(tt,n__zeros) | → | length#(n__zeros) | (19) |
t0 | = | U12#(tt,activate(activate(n__zeros))) |
→R | U12#(tt,activate(n__zeros)) | |
→R | U12#(tt,n__zeros) | |
→P | length#(cons(0,n__zeros)) | |
→P | U11#(tt,activate(n__zeros)) | |
→P | U12#(tt,activate(activate(n__zeros))) | |
= | t5 |