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(X) | (15) |
activate(n__adx(X)) | → | adx(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#(X) | (26) |
activate#(n__adx(X)) | → | adx#(X) | (27) |
activate#(n__0) | → | 0# | (23) |
activate#(n__zeros) | → | zeros# | (24) |
activate#(n__s(X)) | → | s#(X) | (25) |
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)) | → | incr#(X) | (26) |
activate#(n__adx(X)) | → | adx#(X) | (27) |
adx#(cons(X,Y)) | → | incr#(cons(activate(X),n__adx(activate(Y)))) | (20) |
incr#(cons(y_1,n__adx(y_3))) | → | activate#(n__adx(y_3)) | (28) |
t0 | = | adx#(activate(n__zeros)) |
→R | adx#(zeros) | |
→R | adx#(cons(n__0,n__zeros)) | |
→P | incr#(cons(activate(n__0),n__adx(activate(n__zeros)))) | |
→P | activate#(n__adx(activate(n__zeros))) | |
→P | adx#(activate(n__zeros)) | |
= | t5 |