The rewrite relation of the following TRS is considered.
merge(x,nil) | → | x | (1) |
merge(nil,y) | → | y | (2) |
merge(++(x,y),++(u,v)) | → | ++(x,merge(y,++(u,v))) | (3) |
merge(++(x,y),++(u,v)) | → | ++(u,merge(++(x,y),v)) | (4) |
final states:
{0, 1}
transitions:
nil0 | → | 0 |
++0(0,0) | → | 0 |
u0 | → | 0 |
v0 | → | 0 |
merge0(0,0) | → | 1 |
u1 | → | 4 |
v1 | → | 5 |
++1(4,5) | → | 3 |
merge1(0,3) | → | 2 |
++1(0,2) | → | 1 |
++1(0,0) | → | 7 |
v1 | → | 8 |
merge1(7,8) | → | 6 |
++1(4,6) | → | 1 |
++1(0,2) | → | 2 |
++1(4,6) | → | 2 |
0 | → | 1 |
3 | → | 2 |