The rewrite relation of the following TRS is considered.
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#(activate(X1),activate(X2)) |
(36) |
activate#(n__take(X1,X2)) |
→ |
activate#(X1) |
(37) |
activate#(n__take(X1,X2)) |
→ |
activate#(X2) |
(38) |
It remains to prove infiniteness of the resulting DP problem.
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#(activate(X1),activate(X2)) |
(36) |
activate#(n__take(X1,X2)) |
→ |
activate#(X1) |
(37) |
activate#(n__take(X1,X2)) |
→ |
activate#(X2) |
(38) |
and the following rules have been deleted.