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) |
U21(tt,IL,M,N) | → | U22(tt,activate(IL),activate(M),activate(N)) | (4) |
U22(tt,IL,M,N) | → | U23(tt,activate(IL),activate(M),activate(N)) | (5) |
U23(tt,IL,M,N) | → | cons(activate(N),n__take(activate(M),activate(IL))) | (6) |
length(nil) | → | 0 | (7) |
length(cons(N,L)) | → | U11(tt,activate(L)) | (8) |
take(0,IL) | → | nil | (9) |
take(s(M),cons(N,IL)) | → | U21(tt,activate(IL),M,N) | (10) |
zeros | → | n__zeros | (11) |
take(X1,X2) | → | n__take(X1,X2) | (12) |
activate(n__zeros) | → | zeros | (13) |
activate(n__take(X1,X2)) | → | take(X1,X2) | (14) |
activate(X) | → | X | (15) |
length(nil) | → | 0 | (7) |
take(0,IL) | → | nil | (9) |
U11#(tt,L) | → | U12#(tt,activate(L)) | (16) |
U11#(tt,L) | → | activate#(L) | (17) |
U12#(tt,L) | → | length#(activate(L)) | (18) |
U12#(tt,L) | → | activate#(L) | (19) |
U21#(tt,IL,M,N) | → | U22#(tt,activate(IL),activate(M),activate(N)) | (20) |
U21#(tt,IL,M,N) | → | activate#(IL) | (21) |
U21#(tt,IL,M,N) | → | activate#(M) | (22) |
U21#(tt,IL,M,N) | → | activate#(N) | (23) |
U22#(tt,IL,M,N) | → | U23#(tt,activate(IL),activate(M),activate(N)) | (24) |
U22#(tt,IL,M,N) | → | activate#(IL) | (25) |
U22#(tt,IL,M,N) | → | activate#(M) | (26) |
U22#(tt,IL,M,N) | → | activate#(N) | (27) |
U23#(tt,IL,M,N) | → | activate#(N) | (28) |
U23#(tt,IL,M,N) | → | activate#(M) | (29) |
U23#(tt,IL,M,N) | → | activate#(IL) | (30) |
length#(cons(N,L)) | → | U11#(tt,activate(L)) | (31) |
length#(cons(N,L)) | → | activate#(L) | (32) |
take#(s(M),cons(N,IL)) | → | U21#(tt,activate(IL),M,N) | (33) |
take#(s(M),cons(N,IL)) | → | activate#(IL) | (34) |
activate#(n__zeros) | → | zeros# | (35) |
activate#(n__take(X1,X2)) | → | take#(X1,X2) | (36) |
U11#(tt,L) | → | activate#(L) | (17) |
U12#(tt,L) | → | activate#(L) | (19) |
U21#(tt,IL,M,N) | → | U22#(tt,activate(IL),activate(M),activate(N)) | (20) |
U21#(tt,IL,M,N) | → | activate#(IL) | (21) |
U21#(tt,IL,M,N) | → | activate#(M) | (22) |
U21#(tt,IL,M,N) | → | activate#(N) | (23) |
U22#(tt,IL,M,N) | → | U23#(tt,activate(IL),activate(M),activate(N)) | (24) |
U22#(tt,IL,M,N) | → | activate#(IL) | (25) |
U22#(tt,IL,M,N) | → | activate#(M) | (26) |
U22#(tt,IL,M,N) | → | activate#(N) | (27) |
U23#(tt,IL,M,N) | → | activate#(N) | (28) |
U23#(tt,IL,M,N) | → | activate#(M) | (29) |
U23#(tt,IL,M,N) | → | activate#(IL) | (30) |
length#(cons(N,L)) | → | activate#(L) | (32) |
take#(s(M),cons(N,IL)) | → | U21#(tt,activate(IL),M,N) | (33) |
take#(s(M),cons(N,IL)) | → | activate#(IL) | (34) |
activate#(n__zeros) | → | zeros# | (35) |
activate#(n__take(X1,X2)) | → | take#(X1,X2) | (36) |
U11(tt,L) | → | U12(tt,activate(L)) | (2) |
U12(tt,L) | → | s(length(activate(L))) | (3) |
length(cons(N,L)) | → | U11(tt,activate(L)) | (8) |
take(s(M),cons(N,IL)) | → | U21(tt,activate(IL),M,N) | (10) |
U21(tt,IL,M,N) | → | U22(tt,activate(IL),activate(M),activate(N)) | (4) |
U22(tt,IL,M,N) | → | U23(tt,activate(IL),activate(M),activate(N)) | (5) |
U23(tt,IL,M,N) | → | cons(activate(N),n__take(activate(M),activate(IL))) | (6) |
U12#(tt,n__zeros) | → | length#(zeros) | (37) |
U12#(tt,n__take(x0,x1)) | → | length#(take(x0,x1)) | (38) |
U12#(tt,x0) | → | length#(x0) | (39) |
U12#(tt,n__zeros) | → | length#(cons(0,n__zeros)) | (40) |
U12#(tt,n__zeros) | → | length#(n__zeros) | (41) |
U12#(tt,n__zeros) | → | length#(n__zeros) | (41) |
U12#(tt,n__take(x0,x1)) | → | length#(n__take(x0,x1)) | (42) |
U12#(tt,n__take(x0,x1)) | → | length#(n__take(x0,x1)) | (42) |
t0 | = | U11#(tt,activate(n__zeros)) |
→R | U11#(tt,n__zeros) | |
→P | U12#(tt,activate(n__zeros)) | |
→R | U12#(tt,n__zeros) | |
→P | length#(cons(0,n__zeros)) | |
→P | U11#(tt,activate(n__zeros)) | |
= | t5 |