The rewrite relation of the following TRS is considered.
app(nil,YS) | → | YS | (1) |
app(cons(X),YS) | → | cons(X) | (2) |
from(X) | → | cons(X) | (3) |
zWadr(nil,YS) | → | nil | (4) |
zWadr(XS,nil) | → | nil | (5) |
zWadr(cons(X),cons(Y)) | → | cons(app(Y,cons(X))) | (6) |
prefix(L) | → | cons(nil) | (7) |
final states:
{0, 1, 2, 3, 4}
transitions:
nil0 | → | 0 |
cons0(0) | → | 0 |
app0(0,0) | → | 1 |
from0(0) | → | 2 |
zWadr0(0,0) | → | 3 |
prefix0(0) | → | 4 |
cons1(0) | → | 1 |
cons1(0) | → | 2 |
nil1 | → | 3 |
cons1(0) | → | 6 |
app1(0,6) | → | 5 |
cons1(5) | → | 3 |
nil1 | → | 7 |
cons1(7) | → | 4 |
0 | → | 1 |
6 | → | 5 |