The rewrite relation of the following TRS is considered.
addlist(Cons(x,xs'),Cons(S(0),xs)) | → | Cons(S(x),addlist(xs',xs)) | (1) |
addlist(Cons(S(0),xs'),Cons(x,xs)) | → | Cons(S(x),addlist(xs',xs)) | (2) |
addlist(Nil,ys) | → | Nil | (3) |
notEmpty(Cons(x,xs)) | → | True | (4) |
notEmpty(Nil) | → | False | (5) |
goal(xs,ys) | → | addlist(xs,ys) | (6) |
final states:
{0, 1, 2, 3}
transitions:
Cons0(0,0) | → | 0 |
S0(0) | → | 0 |
00 | → | 0 |
Nil0 | → | 0 |
True0 | → | 0 |
False0 | → | 0 |
addlist0(0,0) | → | 1 |
notEmpty0(0) | → | 2 |
goal0(0,0) | → | 3 |
S1(0) | → | 4 |
addlist1(0,0) | → | 5 |
Cons1(4,5) | → | 1 |
Nil1 | → | 1 |
True1 | → | 2 |
False1 | → | 2 |
addlist1(0,0) | → | 3 |
Cons1(4,5) | → | 3 |
Cons1(4,5) | → | 5 |
Nil1 | → | 3 |
Nil1 | → | 5 |