The rewrite relation of the following TRS is considered.
nats | → | adx(zeros) | (1) |
zeros | → | cons(n__0,n__zeros) | (2) |
incr(cons(X,Y)) | → | cons(n__s(activate(X)),n__incr(activate(Y))) | (3) |
adx(cons(X,Y)) | → | incr(cons(activate(X),n__adx(activate(Y)))) | (4) |
hd(cons(X,Y)) | → | activate(X) | (5) |
tl(cons(X,Y)) | → | activate(Y) | (6) |
0 | → | n__0 | (7) |
zeros | → | n__zeros | (8) |
s(X) | → | n__s(X) | (9) |
incr(X) | → | n__incr(X) | (10) |
adx(X) | → | n__adx(X) | (11) |
activate(n__0) | → | 0 | (12) |
activate(n__zeros) | → | zeros | (13) |
activate(n__s(X)) | → | s(X) | (14) |
activate(n__incr(X)) | → | incr(activate(X)) | (15) |
activate(n__adx(X)) | → | adx(activate(X)) | (16) |
activate(X) | → | X | (17) |
nats | → | adx(zeros) | (1) |
hd(cons(X,Y)) | → | activate(X) | (5) |
tl(cons(X,Y)) | → | activate(Y) | (6) |
incr#(cons(X,Y)) | → | activate#(X) | (18) |
incr#(cons(X,Y)) | → | activate#(Y) | (19) |
adx#(cons(X,Y)) | → | incr#(cons(activate(X),n__adx(activate(Y)))) | (20) |
adx#(cons(X,Y)) | → | activate#(X) | (21) |
adx#(cons(X,Y)) | → | activate#(Y) | (22) |
activate#(n__0) | → | 0# | (23) |
activate#(n__zeros) | → | zeros# | (24) |
activate#(n__s(X)) | → | s#(X) | (25) |
activate#(n__incr(X)) | → | incr#(activate(X)) | (26) |
activate#(n__incr(X)) | → | activate#(X) | (27) |
activate#(n__adx(X)) | → | adx#(activate(X)) | (28) |
activate#(n__adx(X)) | → | activate#(X) | (29) |
activate#(n__0) | → | 0# | (23) |
activate#(n__zeros) | → | zeros# | (24) |
activate#(n__s(X)) | → | s#(X) | (25) |
activate#(n__adx(X)) | → | activate#(X) | (29) |
adx#(cons(X,Y)) | → | activate#(X) | (21) |
adx#(cons(X,Y)) | → | activate#(Y) | (22) |
incr#(cons(X,Y)) | → | activate#(X) | (18) |
activate#(n__incr(X)) | → | activate#(X) | (27) |
activate#(n__incr(n__0)) | → | incr#(0) | (30) |
activate#(n__incr(n__zeros)) | → | incr#(zeros) | (31) |
activate#(n__incr(n__s(x0))) | → | incr#(s(x0)) | (32) |
activate#(n__incr(n__incr(x0))) | → | incr#(incr(activate(x0))) | (33) |
activate#(n__incr(n__adx(x0))) | → | incr#(adx(activate(x0))) | (34) |
activate#(n__incr(x0)) | → | incr#(x0) | (35) |
activate#(n__adx(n__0)) | → | adx#(0) | (36) |
activate#(n__adx(n__zeros)) | → | adx#(zeros) | (37) |
activate#(n__adx(n__s(x0))) | → | adx#(s(x0)) | (38) |
activate#(n__adx(n__incr(x0))) | → | adx#(incr(activate(x0))) | (39) |
activate#(n__adx(n__adx(x0))) | → | adx#(adx(activate(x0))) | (40) |
activate#(n__adx(x0)) | → | adx#(x0) | (41) |
activate#(n__incr(n__0)) | → | incr#(n__0) | (42) |
activate#(n__incr(n__0)) | → | incr#(n__0) | (42) |
activate#(n__incr(n__zeros)) | → | incr#(cons(n__0,n__zeros)) | (43) |
activate#(n__incr(n__zeros)) | → | incr#(n__zeros) | (44) |
activate#(n__incr(n__zeros)) | → | incr#(n__zeros) | (44) |
activate#(n__incr(n__s(x0))) | → | incr#(n__s(x0)) | (45) |
activate#(n__incr(n__s(x0))) | → | incr#(n__s(x0)) | (45) |
activate#(n__adx(n__0)) | → | adx#(n__0) | (46) |
activate#(n__adx(n__0)) | → | adx#(n__0) | (46) |
activate#(n__adx(n__zeros)) | → | adx#(cons(n__0,n__zeros)) | (47) |
activate#(n__adx(n__zeros)) | → | adx#(n__zeros) | (48) |
activate#(n__adx(n__zeros)) | → | adx#(n__zeros) | (48) |
activate#(n__adx(n__s(x0))) | → | adx#(n__s(x0)) | (49) |
activate#(n__adx(n__s(x0))) | → | adx#(n__s(x0)) | (49) |
activate#(n__incr(n__zeros)) | → | incr#(cons(n__0,n__zeros)) | (43) |
activate#(n__adx(n__adx(x0))) | → | adx#(adx(activate(x0))) | (40) |
t0 | = | activate#(n__adx(activate(n__zeros))) |
→R | activate#(n__adx(n__zeros)) | |
→P | adx#(cons(n__0,n__zeros)) | |
→P | incr#(cons(activate(n__0),n__adx(activate(n__zeros)))) | |
→P | activate#(n__adx(activate(n__zeros))) | |
= | t4 |