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) |
t0 | = | incr(cons(X,n__adx(cons(x39262,n__zeros)))) |
→ | cons(n__s(activate(X)),n__incr(activate(n__adx(cons(x39262,n__zeros))))) | |
→ | cons(n__s(activate(X)),n__incr(adx(cons(x39262,n__zeros)))) | |
→ | cons(n__s(activate(X)),n__incr(incr(cons(activate(x39262),n__adx(activate(n__zeros)))))) | |
→ | cons(n__s(activate(X)),n__incr(incr(cons(activate(x39262),n__adx(zeros))))) | |
→ | cons(n__s(activate(X)),n__incr(incr(cons(activate(x39262),n__adx(cons(n__0,n__zeros)))))) | |
= | t5 |