The rewrite relation of the following TRS is considered.
app(nil,YS) |
→ |
YS |
(1) |
app(cons(X,XS),YS) |
→ |
cons(X,n__app(activate(XS),YS)) |
(2) |
from(X) |
→ |
cons(X,n__from(n__s(X))) |
(3) |
zWadr(nil,YS) |
→ |
nil |
(4) |
zWadr(XS,nil) |
→ |
nil |
(5) |
zWadr(cons(X,XS),cons(Y,YS)) |
→ |
cons(app(Y,cons(X,n__nil)),n__zWadr(activate(XS),activate(YS))) |
(6) |
prefix(L) |
→ |
cons(nil,n__zWadr(L,n__prefix(L))) |
(7) |
app(X1,X2) |
→ |
n__app(X1,X2) |
(8) |
from(X) |
→ |
n__from(X) |
(9) |
s(X) |
→ |
n__s(X) |
(10) |
nil |
→ |
n__nil |
(11) |
zWadr(X1,X2) |
→ |
n__zWadr(X1,X2) |
(12) |
prefix(X) |
→ |
n__prefix(X) |
(13) |
activate(n__app(X1,X2)) |
→ |
app(activate(X1),activate(X2)) |
(14) |
activate(n__from(X)) |
→ |
from(activate(X)) |
(15) |
activate(n__s(X)) |
→ |
s(activate(X)) |
(16) |
activate(n__nil) |
→ |
nil |
(17) |
activate(n__zWadr(X1,X2)) |
→ |
zWadr(activate(X1),activate(X2)) |
(18) |
activate(n__prefix(X)) |
→ |
prefix(activate(X)) |
(19) |
activate(X) |
→ |
X |
(20) |
app#(cons(X,XS),YS) |
→ |
activate#(XS) |
(21) |
zWadr#(cons(X,XS),cons(Y,YS)) |
→ |
app#(Y,cons(X,n__nil)) |
(22) |
zWadr#(cons(X,XS),cons(Y,YS)) |
→ |
activate#(XS) |
(23) |
zWadr#(cons(X,XS),cons(Y,YS)) |
→ |
activate#(YS) |
(24) |
prefix#(L) |
→ |
nil# |
(25) |
activate#(n__app(X1,X2)) |
→ |
app#(activate(X1),activate(X2)) |
(26) |
activate#(n__app(X1,X2)) |
→ |
activate#(X1) |
(27) |
activate#(n__app(X1,X2)) |
→ |
activate#(X2) |
(28) |
activate#(n__from(X)) |
→ |
from#(activate(X)) |
(29) |
activate#(n__from(X)) |
→ |
activate#(X) |
(30) |
activate#(n__s(X)) |
→ |
s#(activate(X)) |
(31) |
activate#(n__s(X)) |
→ |
activate#(X) |
(32) |
activate#(n__nil) |
→ |
nil# |
(33) |
activate#(n__zWadr(X1,X2)) |
→ |
zWadr#(activate(X1),activate(X2)) |
(34) |
activate#(n__zWadr(X1,X2)) |
→ |
activate#(X1) |
(35) |
activate#(n__zWadr(X1,X2)) |
→ |
activate#(X2) |
(36) |
activate#(n__prefix(X)) |
→ |
prefix#(activate(X)) |
(37) |
activate#(n__prefix(X)) |
→ |
activate#(X) |
(38) |
It remains to prove infiniteness of the resulting DP problem.
activate#(n__zWadr(n__app(x0,x1),y1)) |
→ |
zWadr#(app(activate(x0),activate(x1)),activate(y1)) |
(39) |
activate#(n__zWadr(n__from(x0),y1)) |
→ |
zWadr#(from(activate(x0)),activate(y1)) |
(40) |
activate#(n__zWadr(n__s(x0),y1)) |
→ |
zWadr#(s(activate(x0)),activate(y1)) |
(41) |
activate#(n__zWadr(n__nil,y1)) |
→ |
zWadr#(nil,activate(y1)) |
(42) |
activate#(n__zWadr(n__zWadr(x0,x1),y1)) |
→ |
zWadr#(zWadr(activate(x0),activate(x1)),activate(y1)) |
(43) |
activate#(n__zWadr(n__prefix(x0),y1)) |
→ |
zWadr#(prefix(activate(x0)),activate(y1)) |
(44) |
activate#(n__zWadr(x0,y1)) |
→ |
zWadr#(x0,activate(y1)) |
(45) |
activate#(n__zWadr(n__app(y0,y1),n__app(x0,x1))) |
→ |
zWadr#(app(activate(y0),activate(y1)),app(activate(x0),activate(x1))) |
(46) |
activate#(n__zWadr(n__app(y0,y1),n__from(x0))) |
→ |
zWadr#(app(activate(y0),activate(y1)),from(activate(x0))) |
(47) |
activate#(n__zWadr(n__app(y0,y1),n__s(x0))) |
→ |
zWadr#(app(activate(y0),activate(y1)),s(activate(x0))) |
(48) |
activate#(n__zWadr(n__app(y0,y1),n__nil)) |
→ |
zWadr#(app(activate(y0),activate(y1)),nil) |
(49) |
activate#(n__zWadr(n__app(y0,y1),n__zWadr(x0,x1))) |
→ |
zWadr#(app(activate(y0),activate(y1)),zWadr(activate(x0),activate(x1))) |
(50) |
activate#(n__zWadr(n__app(y0,y1),n__prefix(x0))) |
→ |
zWadr#(app(activate(y0),activate(y1)),prefix(activate(x0))) |
(51) |
activate#(n__zWadr(n__app(y0,y1),x0)) |
→ |
zWadr#(app(activate(y0),activate(y1)),x0) |
(52) |
activate#(n__zWadr(n__from(y0),n__app(x0,x1))) |
→ |
zWadr#(from(activate(y0)),app(activate(x0),activate(x1))) |
(53) |
activate#(n__zWadr(n__from(y0),n__from(x0))) |
→ |
zWadr#(from(activate(y0)),from(activate(x0))) |
(54) |
activate#(n__zWadr(n__from(y0),n__s(x0))) |
→ |
zWadr#(from(activate(y0)),s(activate(x0))) |
(55) |
activate#(n__zWadr(n__from(y0),n__nil)) |
→ |
zWadr#(from(activate(y0)),nil) |
(56) |
activate#(n__zWadr(n__from(y0),n__zWadr(x0,x1))) |
→ |
zWadr#(from(activate(y0)),zWadr(activate(x0),activate(x1))) |
(57) |
activate#(n__zWadr(n__from(y0),n__prefix(x0))) |
→ |
zWadr#(from(activate(y0)),prefix(activate(x0))) |
(58) |
activate#(n__zWadr(n__from(y0),x0)) |
→ |
zWadr#(from(activate(y0)),x0) |
(59) |
activate#(n__zWadr(n__s(y0),n__app(x0,x1))) |
→ |
zWadr#(s(activate(y0)),app(activate(x0),activate(x1))) |
(60) |
activate#(n__zWadr(n__s(y0),n__from(x0))) |
→ |
zWadr#(s(activate(y0)),from(activate(x0))) |
(61) |
activate#(n__zWadr(n__s(y0),n__s(x0))) |
→ |
zWadr#(s(activate(y0)),s(activate(x0))) |
(62) |
activate#(n__zWadr(n__s(y0),n__nil)) |
→ |
zWadr#(s(activate(y0)),nil) |
(63) |
activate#(n__zWadr(n__s(y0),n__zWadr(x0,x1))) |
→ |
zWadr#(s(activate(y0)),zWadr(activate(x0),activate(x1))) |
(64) |
activate#(n__zWadr(n__s(y0),n__prefix(x0))) |
→ |
zWadr#(s(activate(y0)),prefix(activate(x0))) |
(65) |
activate#(n__zWadr(n__s(y0),x0)) |
→ |
zWadr#(s(activate(y0)),x0) |
(66) |
activate#(n__zWadr(n__zWadr(y0,y1),n__app(x0,x1))) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),app(activate(x0),activate(x1))) |
(68) |
activate#(n__zWadr(n__zWadr(y0,y1),n__from(x0))) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),from(activate(x0))) |
(69) |
activate#(n__zWadr(n__zWadr(y0,y1),n__s(x0))) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),s(activate(x0))) |
(70) |
activate#(n__zWadr(n__zWadr(y0,y1),n__nil)) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),nil) |
(71) |
activate#(n__zWadr(n__zWadr(y0,y1),n__zWadr(x0,x1))) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),zWadr(activate(x0),activate(x1))) |
(72) |
activate#(n__zWadr(n__zWadr(y0,y1),n__prefix(x0))) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),prefix(activate(x0))) |
(73) |
activate#(n__zWadr(n__zWadr(y0,y1),x0)) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),x0) |
(74) |
activate#(n__zWadr(n__prefix(y0),n__app(x0,x1))) |
→ |
zWadr#(prefix(activate(y0)),app(activate(x0),activate(x1))) |
(75) |
activate#(n__zWadr(n__prefix(y0),n__from(x0))) |
→ |
zWadr#(prefix(activate(y0)),from(activate(x0))) |
(76) |
activate#(n__zWadr(n__prefix(y0),n__s(x0))) |
→ |
zWadr#(prefix(activate(y0)),s(activate(x0))) |
(77) |
activate#(n__zWadr(n__prefix(y0),n__nil)) |
→ |
zWadr#(prefix(activate(y0)),nil) |
(78) |
activate#(n__zWadr(n__prefix(y0),n__zWadr(x0,x1))) |
→ |
zWadr#(prefix(activate(y0)),zWadr(activate(x0),activate(x1))) |
(79) |
activate#(n__zWadr(n__prefix(y0),n__prefix(x0))) |
→ |
zWadr#(prefix(activate(y0)),prefix(activate(x0))) |
(80) |
activate#(n__zWadr(n__prefix(y0),x0)) |
→ |
zWadr#(prefix(activate(y0)),x0) |
(81) |
activate#(n__zWadr(y0,n__app(x0,x1))) |
→ |
zWadr#(y0,app(activate(x0),activate(x1))) |
(82) |
activate#(n__zWadr(y0,n__from(x0))) |
→ |
zWadr#(y0,from(activate(x0))) |
(83) |
activate#(n__zWadr(y0,n__s(x0))) |
→ |
zWadr#(y0,s(activate(x0))) |
(84) |
activate#(n__zWadr(y0,n__nil)) |
→ |
zWadr#(y0,nil) |
(85) |
activate#(n__zWadr(y0,n__zWadr(x0,x1))) |
→ |
zWadr#(y0,zWadr(activate(x0),activate(x1))) |
(86) |
activate#(n__zWadr(y0,n__prefix(x0))) |
→ |
zWadr#(y0,prefix(activate(x0))) |
(87) |
activate#(n__zWadr(y0,x0)) |
→ |
zWadr#(y0,x0) |
(88) |
activate#(n__zWadr(n__app(y0,y1),n__from(x0))) |
→ |
zWadr#(app(activate(y0),activate(y1)),from(activate(x0))) |
(47) |
activate#(n__zWadr(n__app(y0,y1),n__s(x0))) |
→ |
zWadr#(app(activate(y0),activate(y1)),s(activate(x0))) |
(48) |
activate#(n__zWadr(n__from(y0),n__from(x0))) |
→ |
zWadr#(from(activate(y0)),from(activate(x0))) |
(54) |
activate#(n__zWadr(n__from(y0),n__s(x0))) |
→ |
zWadr#(from(activate(y0)),s(activate(x0))) |
(55) |
activate#(n__zWadr(n__s(y0),n__from(x0))) |
→ |
zWadr#(s(activate(y0)),from(activate(x0))) |
(61) |
activate#(n__zWadr(n__s(y0),n__s(x0))) |
→ |
zWadr#(s(activate(y0)),s(activate(x0))) |
(62) |
activate#(n__zWadr(n__zWadr(y0,y1),n__from(x0))) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),from(activate(x0))) |
(69) |
activate#(n__zWadr(n__zWadr(y0,y1),n__s(x0))) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),s(activate(x0))) |
(70) |
activate#(n__zWadr(n__prefix(y0),n__from(x0))) |
→ |
zWadr#(prefix(activate(y0)),from(activate(x0))) |
(76) |
activate#(n__zWadr(n__prefix(y0),n__s(x0))) |
→ |
zWadr#(prefix(activate(y0)),s(activate(x0))) |
(77) |
activate#(n__zWadr(y0,n__from(x0))) |
→ |
zWadr#(y0,from(activate(x0))) |
(83) |
activate#(n__zWadr(y0,n__s(x0))) |
→ |
zWadr#(y0,s(activate(x0))) |
(84) |
and the following rules have been deleted.
activate#(n__zWadr(n__app(y0,y1),n__app(x0,x1))) |
→ |
zWadr#(app(activate(y0),activate(y1)),app(activate(x0),activate(x1))) |
(46) |
activate#(n__zWadr(n__from(y0),n__app(x0,x1))) |
→ |
zWadr#(from(activate(y0)),app(activate(x0),activate(x1))) |
(53) |
activate#(n__zWadr(n__s(y0),n__app(x0,x1))) |
→ |
zWadr#(s(activate(y0)),app(activate(x0),activate(x1))) |
(60) |
activate#(n__zWadr(n__zWadr(y0,y1),n__app(x0,x1))) |
→ |
zWadr#(zWadr(activate(y0),activate(y1)),app(activate(x0),activate(x1))) |
(68) |
activate#(n__zWadr(n__prefix(y0),n__app(x0,x1))) |
→ |
zWadr#(prefix(activate(y0)),app(activate(x0),activate(x1))) |
(75) |
activate#(n__zWadr(y0,n__app(x0,x1))) |
→ |
zWadr#(y0,app(activate(x0),activate(x1))) |
(82) |
and the following rules have been deleted.
t0
|
= |
zWadr#(from(X'),prefix(activate(n__from(y0)))) |
|
→R
|
zWadr#(from(X'),prefix(n__from(y0))) |
|
→R
|
zWadr#(from(X'),cons(nil,n__zWadr(n__from(y0),n__prefix(n__from(y0))))) |
|
→R
|
zWadr#(cons(X',n__from(n__s(X'))),cons(nil,n__zWadr(n__from(y0),n__prefix(n__from(y0))))) |
|
→P
|
activate#(n__zWadr(n__from(y0),n__prefix(n__from(y0)))) |
|
→P
|
zWadr#(from(activate(y0)),prefix(activate(n__from(y0)))) |
|
= |
t5
|
where t