The rewrite relation of the following TRS is considered.
list(Cons(x,xs)) | → | list(xs) | (1) |
list(Nil) | → | True | (2) |
list(Nil) | → | isEmpty[Match](Nil) | (3) |
notEmpty(Cons(x,xs)) | → | True | (4) |
notEmpty(Nil) | → | False | (5) |
goal(x) | → | list(x) | (6) |
final states:
{0, 1, 2, 3}
transitions:
Cons0(0,0) | → | 0 |
Nil0 | → | 0 |
True0 | → | 0 |
isEmpty[Match]0(0) | → | 0 |
False0 | → | 0 |
list0(0) | → | 1 |
notEmpty0(0) | → | 2 |
goal0(0) | → | 3 |
list1(0) | → | 1 |
True1 | → | 1 |
Nil1 | → | 4 |
isEmpty[Match]1(4) | → | 1 |
True1 | → | 2 |
False1 | → | 2 |
list1(0) | → | 3 |
True1 | → | 3 |
isEmpty[Match]1(4) | → | 3 |