The rewrite relation of the following TRS is considered.
eq(n__0,n__0) | → | true | (1) |
eq(n__s(X),n__s(Y)) | → | eq(activate(X),activate(Y)) | (2) |
eq(X,Y) | → | false | (3) |
inf(X) | → | cons(X,n__inf(s(X))) | (4) |
take(0,X) | → | nil | (5) |
take(s(X),cons(Y,L)) | → | cons(activate(Y),n__take(activate(X),activate(L))) | (6) |
length(nil) | → | 0 | (7) |
length(cons(X,L)) | → | s(n__length(activate(L))) | (8) |
0 | → | n__0 | (9) |
s(X) | → | n__s(X) | (10) |
inf(X) | → | n__inf(X) | (11) |
take(X1,X2) | → | n__take(X1,X2) | (12) |
length(X) | → | n__length(X) | (13) |
activate(n__0) | → | 0 | (14) |
activate(n__s(X)) | → | s(X) | (15) |
activate(n__inf(X)) | → | inf(X) | (16) |
activate(n__take(X1,X2)) | → | take(X1,X2) | (17) |
activate(n__length(X)) | → | length(X) | (18) |
activate(X) | → | X | (19) |
eq#(n__s(X),n__s(Y)) | → | eq#(activate(X),activate(Y)) | (20) |
eq#(n__s(X),n__s(Y)) | → | activate#(X) | (21) |
eq#(n__s(X),n__s(Y)) | → | activate#(Y) | (22) |
inf#(X) | → | s#(X) | (23) |
take#(s(X),cons(Y,L)) | → | activate#(Y) | (24) |
take#(s(X),cons(Y,L)) | → | activate#(X) | (25) |
take#(s(X),cons(Y,L)) | → | activate#(L) | (26) |
length#(nil) | → | 0# | (27) |
length#(cons(X,L)) | → | s#(n__length(activate(L))) | (28) |
length#(cons(X,L)) | → | activate#(L) | (29) |
activate#(n__0) | → | 0# | (30) |
activate#(n__s(X)) | → | s#(X) | (31) |
activate#(n__inf(X)) | → | inf#(X) | (32) |
activate#(n__take(X1,X2)) | → | take#(X1,X2) | (33) |
activate#(n__length(X)) | → | length#(X) | (34) |
eq#(n__s(X),n__s(Y)) | → | activate#(X) | (21) |
eq#(n__s(X),n__s(Y)) | → | activate#(Y) | (22) |
inf#(X) | → | s#(X) | (23) |
take#(s(X),cons(Y,L)) | → | activate#(Y) | (24) |
take#(s(X),cons(Y,L)) | → | activate#(X) | (25) |
take#(s(X),cons(Y,L)) | → | activate#(L) | (26) |
length#(nil) | → | 0# | (27) |
length#(cons(X,L)) | → | s#(n__length(activate(L))) | (28) |
length#(cons(X,L)) | → | activate#(L) | (29) |
activate#(n__0) | → | 0# | (30) |
activate#(n__s(X)) | → | s#(X) | (31) |
activate#(n__inf(X)) | → | inf#(X) | (32) |
activate#(n__take(X1,X2)) | → | take#(X1,X2) | (33) |
activate#(n__length(X)) | → | length#(X) | (34) |
eq#(n__s(n__0),n__s(y1)) | → | eq#(0,activate(y1)) | (35) |
eq#(n__s(n__s(x0)),n__s(y1)) | → | eq#(s(x0),activate(y1)) | (36) |
eq#(n__s(n__inf(x0)),n__s(y1)) | → | eq#(inf(x0),activate(y1)) | (37) |
eq#(n__s(n__take(x0,x1)),n__s(y1)) | → | eq#(take(x0,x1),activate(y1)) | (38) |
eq#(n__s(n__length(x0)),n__s(y1)) | → | eq#(length(x0),activate(y1)) | (39) |
eq#(n__s(x0),n__s(y1)) | → | eq#(x0,activate(y1)) | (40) |
eq#(n__s(n__0),n__s(y0)) | → | eq#(n__0,activate(y0)) | (41) |
eq#(n__s(n__0),n__s(y0)) | → | eq#(n__0,activate(y0)) | (41) |
eq#(n__s(n__s(x0)),n__s(y1)) | → | eq#(n__s(x0),activate(y1)) | (42) |
eq#(n__s(n__inf(x0)),n__s(y1)) | → | eq#(cons(x0,n__inf(s(x0))),activate(y1)) | (43) |
eq#(n__s(n__inf(x0)),n__s(y1)) | → | eq#(n__inf(x0),activate(y1)) | (44) |
eq#(n__s(n__inf(x0)),n__s(y1)) | → | eq#(cons(x0,n__inf(s(x0))),activate(y1)) | (43) |
eq#(n__s(n__inf(x0)),n__s(y1)) | → | eq#(n__inf(x0),activate(y1)) | (44) |
eq#(n__s(n__take(y0,y1)),n__s(n__0)) | → | eq#(take(y0,y1),0) | (45) |
eq#(n__s(n__take(y0,y1)),n__s(n__s(x0))) | → | eq#(take(y0,y1),s(x0)) | (46) |
eq#(n__s(n__take(y0,y1)),n__s(n__inf(x0))) | → | eq#(take(y0,y1),inf(x0)) | (47) |
eq#(n__s(n__take(y0,y1)),n__s(n__take(x0,x1))) | → | eq#(take(y0,y1),take(x0,x1)) | (48) |
eq#(n__s(n__take(y0,y1)),n__s(n__length(x0))) | → | eq#(take(y0,y1),length(x0)) | (49) |
eq#(n__s(n__take(y0,y1)),n__s(x0)) | → | eq#(take(y0,y1),x0) | (50) |
eq#(n__s(n__length(y0)),n__s(n__0)) | → | eq#(length(y0),0) | (51) |
eq#(n__s(n__length(y0)),n__s(n__s(x0))) | → | eq#(length(y0),s(x0)) | (52) |
eq#(n__s(n__length(y0)),n__s(n__inf(x0))) | → | eq#(length(y0),inf(x0)) | (53) |
eq#(n__s(n__length(y0)),n__s(n__take(x0,x1))) | → | eq#(length(y0),take(x0,x1)) | (54) |
eq#(n__s(n__length(y0)),n__s(n__length(x0))) | → | eq#(length(y0),length(x0)) | (55) |
eq#(n__s(n__length(y0)),n__s(x0)) | → | eq#(length(y0),x0) | (56) |
eq#(n__s(y0),n__s(n__0)) | → | eq#(y0,0) | (57) |
eq#(n__s(y0),n__s(n__s(x0))) | → | eq#(y0,s(x0)) | (58) |
eq#(n__s(y0),n__s(n__inf(x0))) | → | eq#(y0,inf(x0)) | (59) |
eq#(n__s(y0),n__s(n__take(x0,x1))) | → | eq#(y0,take(x0,x1)) | (60) |
eq#(n__s(y0),n__s(n__length(x0))) | → | eq#(y0,length(x0)) | (61) |
eq#(n__s(y0),n__s(x0)) | → | eq#(y0,x0) | (62) |
eq#(n__s(n__take(y0,y1)),n__s(n__0)) | → | eq#(take(y0,y1),n__0) | (63) |
eq#(n__s(n__take(y0,y1)),n__s(n__0)) | → | eq#(take(y0,y1),n__0) | (63) |
eq#(n__s(n__take(y0,y1)),n__s(n__s(x0))) | → | eq#(take(y0,y1),n__s(x0)) | (64) |
eq#(n__s(n__take(y0,y1)),n__s(n__inf(x0))) | → | eq#(take(y0,y1),cons(x0,n__inf(s(x0)))) | (65) |
eq#(n__s(n__take(y0,y1)),n__s(n__inf(x0))) | → | eq#(take(y0,y1),n__inf(x0)) | (66) |
eq#(n__s(n__take(y0,y1)),n__s(n__inf(x0))) | → | eq#(take(y0,y1),cons(x0,n__inf(s(x0)))) | (65) |
eq#(n__s(n__take(y0,y1)),n__s(n__inf(x0))) | → | eq#(take(y0,y1),n__inf(x0)) | (66) |
eq#(n__s(n__length(y0)),n__s(n__0)) | → | eq#(length(y0),n__0) | (67) |
eq#(n__s(n__length(y0)),n__s(n__0)) | → | eq#(length(y0),n__0) | (67) |
eq#(n__s(n__length(y0)),n__s(n__s(x0))) | → | eq#(length(y0),n__s(x0)) | (68) |
eq#(n__s(n__length(y0)),n__s(n__inf(x0))) | → | eq#(length(y0),cons(x0,n__inf(s(x0)))) | (69) |
eq#(n__s(n__length(y0)),n__s(n__inf(x0))) | → | eq#(length(y0),n__inf(x0)) | (70) |
eq#(n__s(n__length(y0)),n__s(n__inf(x0))) | → | eq#(length(y0),cons(x0,n__inf(s(x0)))) | (69) |
eq#(n__s(n__length(y0)),n__s(n__inf(x0))) | → | eq#(length(y0),n__inf(x0)) | (70) |
eq#(n__s(y0),n__s(n__0)) | → | eq#(y0,n__0) | (71) |
eq#(n__s(y0),n__s(n__0)) | → | eq#(y0,n__0) | (71) |
eq#(n__s(y0),n__s(n__s(x0))) | → | eq#(y0,n__s(x0)) | (72) |
eq#(n__s(y0),n__s(n__inf(x0))) | → | eq#(y0,cons(x0,n__inf(s(x0)))) | (73) |
eq#(n__s(y0),n__s(n__inf(x0))) | → | eq#(y0,n__inf(x0)) | (74) |
eq#(n__s(y0),n__s(n__inf(x0))) | → | eq#(y0,cons(x0,n__inf(s(x0)))) | (73) |
eq#(n__s(y0),n__s(n__inf(x0))) | → | eq#(y0,n__inf(x0)) | (74) |
eq#(n__s(n__take(y0,y1)),n__s(n__take(x0,x1))) | → | eq#(take(y0,y1),take(x0,x1)) | (48) |
eq#(n__s(n__length(y0)),n__s(n__take(x0,x1))) | → | eq#(length(y0),take(x0,x1)) | (54) |
eq#(n__s(y0),n__s(n__take(x0,x1))) | → | eq#(y0,take(x0,x1)) | (60) |
eq#(n__s(n__s(x0)),n__s(y1)) | → | eq#(n__s(x0),activate(y1)) | (42) |
eq#(n__s(n__take(y0,y1)),n__s(n__length(x0))) | → | eq#(take(y0,y1),length(x0)) | (49) |
eq#(n__s(n__take(y0,y1)),n__s(x0)) | → | eq#(take(y0,y1),x0) | (50) |
eq#(n__s(y0),n__s(n__length(x0))) | → | eq#(y0,length(x0)) | (61) |
eq#(n__s(y0),n__s(x0)) | → | eq#(y0,x0) | (62) |
eq#(n__s(n__take(y0,y1)),n__s(n__s(x0))) | → | eq#(take(y0,y1),n__s(x0)) | (64) |
eq#(n__s(y0),n__s(n__s(x0))) | → | eq#(y0,n__s(x0)) | (72) |
eq#(n__s(n__length(y0)),n__s(x0)) | → | eq#(length(y0),x0) | (56) |
eq#(n__s(n__length(y0)),n__s(n__s(x0))) | → | eq#(length(y0),n__s(x0)) | (68) |
t0 | = | eq#(length(activate(n__inf(X))),length(activate(n__inf(X')))) |
→R | eq#(length(activate(n__inf(X))),length(inf(X'))) | |
→R | eq#(length(activate(n__inf(X))),length(cons(X',n__inf(s(X'))))) | |
→R | eq#(length(activate(n__inf(X))),s(n__length(activate(n__inf(s(X')))))) | |
→R | eq#(length(activate(n__inf(X))),n__s(n__length(activate(n__inf(s(X')))))) | |
→R | eq#(length(inf(X)),n__s(n__length(activate(n__inf(s(X')))))) | |
→R | eq#(length(cons(X,n__inf(s(X)))),n__s(n__length(activate(n__inf(s(X')))))) | |
→R | eq#(s(n__length(activate(n__inf(s(X))))),n__s(n__length(activate(n__inf(s(X')))))) | |
→R | eq#(n__s(n__length(activate(n__inf(s(X))))),n__s(n__length(activate(n__inf(s(X')))))) | |
→P | eq#(length(activate(n__inf(s(X)))),length(activate(n__inf(s(X'))))) | |
= | t9 |