The rewrite relation of the following TRS is considered.
eq#(n__s(n__0),n__s(y1)) |
→ |
eq#(0,activate(y1)) |
(38) |
eq#(n__s(n__s(x0)),n__s(y1)) |
→ |
eq#(s(x0),activate(y1)) |
(39) |
eq#(n__s(n__inf(x0)),n__s(y1)) |
→ |
eq#(inf(activate(x0)),activate(y1)) |
(40) |
eq#(n__s(n__take(x0,x1)),n__s(y1)) |
→ |
eq#(take(activate(x0),activate(x1)),activate(y1)) |
(41) |
eq#(n__s(n__length(x0)),n__s(y1)) |
→ |
eq#(length(activate(x0)),activate(y1)) |
(42) |
eq#(n__s(x0),n__s(y1)) |
→ |
eq#(x0,activate(y1)) |
(43) |
eq#(n__s(n__inf(y0)),n__s(n__0)) |
→ |
eq#(inf(activate(y0)),0) |
(46) |
eq#(n__s(n__inf(y0)),n__s(n__s(x0))) |
→ |
eq#(inf(activate(y0)),s(x0)) |
(47) |
eq#(n__s(n__inf(y0)),n__s(n__inf(x0))) |
→ |
eq#(inf(activate(y0)),inf(activate(x0))) |
(48) |
eq#(n__s(n__inf(y0)),n__s(n__take(x0,x1))) |
→ |
eq#(inf(activate(y0)),take(activate(x0),activate(x1))) |
(49) |
eq#(n__s(n__inf(y0)),n__s(n__length(x0))) |
→ |
eq#(inf(activate(y0)),length(activate(x0))) |
(50) |
eq#(n__s(n__inf(y0)),n__s(x0)) |
→ |
eq#(inf(activate(y0)),x0) |
(51) |
eq#(n__s(n__take(y0,y1)),n__s(n__0)) |
→ |
eq#(take(activate(y0),activate(y1)),0) |
(52) |
eq#(n__s(n__take(y0,y1)),n__s(n__s(x0))) |
→ |
eq#(take(activate(y0),activate(y1)),s(x0)) |
(53) |
eq#(n__s(n__take(y0,y1)),n__s(n__inf(x0))) |
→ |
eq#(take(activate(y0),activate(y1)),inf(activate(x0))) |
(54) |
eq#(n__s(n__take(y0,y1)),n__s(n__take(x0,x1))) |
→ |
eq#(take(activate(y0),activate(y1)),take(activate(x0),activate(x1))) |
(55) |
eq#(n__s(n__take(y0,y1)),n__s(n__length(x0))) |
→ |
eq#(take(activate(y0),activate(y1)),length(activate(x0))) |
(56) |
eq#(n__s(n__take(y0,y1)),n__s(x0)) |
→ |
eq#(take(activate(y0),activate(y1)),x0) |
(57) |
eq#(n__s(n__length(y0)),n__s(n__0)) |
→ |
eq#(length(activate(y0)),0) |
(58) |
eq#(n__s(n__length(y0)),n__s(n__s(x0))) |
→ |
eq#(length(activate(y0)),s(x0)) |
(59) |
eq#(n__s(n__length(y0)),n__s(n__inf(x0))) |
→ |
eq#(length(activate(y0)),inf(activate(x0))) |
(60) |
eq#(n__s(n__length(y0)),n__s(n__take(x0,x1))) |
→ |
eq#(length(activate(y0)),take(activate(x0),activate(x1))) |
(61) |
eq#(n__s(n__length(y0)),n__s(n__length(x0))) |
→ |
eq#(length(activate(y0)),length(activate(x0))) |
(62) |
eq#(n__s(n__length(y0)),n__s(x0)) |
→ |
eq#(length(activate(y0)),x0) |
(63) |
eq#(n__s(y0),n__s(n__0)) |
→ |
eq#(y0,0) |
(64) |
eq#(n__s(y0),n__s(n__s(x0))) |
→ |
eq#(y0,s(x0)) |
(65) |
eq#(n__s(y0),n__s(n__inf(x0))) |
→ |
eq#(y0,inf(activate(x0))) |
(66) |
eq#(n__s(y0),n__s(n__take(x0,x1))) |
→ |
eq#(y0,take(activate(x0),activate(x1))) |
(67) |
eq#(n__s(y0),n__s(n__length(x0))) |
→ |
eq#(y0,length(activate(x0))) |
(68) |
eq#(n__s(y0),n__s(x0)) |
→ |
eq#(y0,x0) |
(69) |
eq#(n__s(n__s(x0)),n__s(y1)) |
→ |
eq#(n__s(x0),activate(y1)) |
(45) |
eq#(n__s(n__inf(y0)),n__s(n__inf(x0))) |
→ |
eq#(inf(activate(y0)),inf(activate(x0))) |
(48) |
eq#(n__s(n__inf(y0)),n__s(n__take(x0,x1))) |
→ |
eq#(inf(activate(y0)),take(activate(x0),activate(x1))) |
(49) |
eq#(n__s(n__inf(y0)),n__s(n__length(x0))) |
→ |
eq#(inf(activate(y0)),length(activate(x0))) |
(50) |
eq#(n__s(n__inf(y0)),n__s(x0)) |
→ |
eq#(inf(activate(y0)),x0) |
(51) |
eq#(n__s(n__take(y0,y1)),n__s(n__inf(x0))) |
→ |
eq#(take(activate(y0),activate(y1)),inf(activate(x0))) |
(54) |
eq#(n__s(n__take(y0,y1)),n__s(n__take(x0,x1))) |
→ |
eq#(take(activate(y0),activate(y1)),take(activate(x0),activate(x1))) |
(55) |
eq#(n__s(n__take(y0,y1)),n__s(n__length(x0))) |
→ |
eq#(take(activate(y0),activate(y1)),length(activate(x0))) |
(56) |
eq#(n__s(n__take(y0,y1)),n__s(x0)) |
→ |
eq#(take(activate(y0),activate(y1)),x0) |
(57) |
eq#(n__s(y0),n__s(n__inf(x0))) |
→ |
eq#(y0,inf(activate(x0))) |
(66) |
eq#(n__s(y0),n__s(n__take(x0,x1))) |
→ |
eq#(y0,take(activate(x0),activate(x1))) |
(67) |
eq#(n__s(y0),n__s(n__length(x0))) |
→ |
eq#(y0,length(activate(x0))) |
(68) |
eq#(n__s(y0),n__s(x0)) |
→ |
eq#(y0,x0) |
(69) |
eq#(n__s(n__inf(y0)),n__s(n__s(x0))) |
→ |
eq#(inf(activate(y0)),n__s(x0)) |
(71) |
eq#(n__s(n__take(y0,y1)),n__s(n__s(x0))) |
→ |
eq#(take(activate(y0),activate(y1)),n__s(x0)) |
(73) |
eq#(n__s(y0),n__s(n__s(x0))) |
→ |
eq#(y0,n__s(x0)) |
(77) |
and the following rules have been deleted.
eq#(n__s(n__length(y0)),n__s(n__inf(x0))) |
→ |
eq#(length(activate(y0)),inf(activate(x0))) |
(60) |
eq#(n__s(n__length(y0)),n__s(n__take(x0,x1))) |
→ |
eq#(length(activate(y0)),take(activate(x0),activate(x1))) |
(61) |
eq#(n__s(n__length(y0)),n__s(x0)) |
→ |
eq#(length(activate(y0)),x0) |
(63) |
eq#(n__s(n__length(y0)),n__s(n__s(x0))) |
→ |
eq#(length(activate(y0)),n__s(x0)) |
(75) |
and the following rules have been deleted.
t0
|
= |
eq#(length(activate(activate(n__inf(X)))),length(activate(activate(n__inf(X'))))) |
|
→R
|
eq#(length(activate(activate(n__inf(X)))),length(activate(n__inf(X')))) |
|
→R
|
eq#(length(activate(activate(n__inf(X)))),length(inf(activate(X')))) |
|
→R
|
eq#(length(activate(activate(n__inf(X)))),length(cons(activate(X'),n__inf(n__s(activate(X')))))) |
|
→R
|
eq#(length(activate(activate(n__inf(X)))),s(n__length(activate(n__inf(n__s(activate(X'))))))) |
|
→R
|
eq#(length(activate(activate(n__inf(X)))),n__s(n__length(activate(n__inf(n__s(activate(X'))))))) |
|
→R
|
eq#(length(activate(n__inf(X))),n__s(n__length(activate(n__inf(n__s(activate(X'))))))) |
|
→R
|
eq#(length(inf(activate(X))),n__s(n__length(activate(n__inf(n__s(activate(X'))))))) |
|
→R
|
eq#(length(cons(activate(X),n__inf(n__s(activate(X))))),n__s(n__length(activate(n__inf(n__s(activate(X'))))))) |
|
→R
|
eq#(s(n__length(activate(n__inf(n__s(activate(X)))))),n__s(n__length(activate(n__inf(n__s(activate(X'))))))) |
|
→R
|
eq#(n__s(n__length(activate(n__inf(n__s(activate(X)))))),n__s(n__length(activate(n__inf(n__s(activate(X'))))))) |
|
→P
|
eq#(length(activate(activate(n__inf(n__s(activate(X)))))),length(activate(activate(n__inf(n__s(activate(X'))))))) |
|
= |
t11
|
where t