The rewrite relation of the following TRS is considered.
| odd(Cons(x,xs)) | → | even(xs) | (1) |
| odd(Nil) | → | False | (2) |
| even(Cons(x,xs)) | → | odd(xs) | (3) |
| notEmpty(Cons(x,xs)) | → | True | (4) |
| notEmpty(Nil) | → | False | (5) |
| even(Nil) | → | True | (6) |
| evenodd(x) | → | even(x) | (7) |
final states:
{0, 1, 2, 3, 4}
transitions:
| Cons0(0,0) | → | 0 |
| Nil0 | → | 0 |
| False0 | → | 0 |
| True0 | → | 0 |
| odd0(0) | → | 1 |
| even0(0) | → | 2 |
| notEmpty0(0) | → | 3 |
| evenodd0(0) | → | 4 |
| even1(0) | → | 1 |
| False1 | → | 1 |
| odd1(0) | → | 2 |
| True1 | → | 3 |
| False1 | → | 3 |
| True1 | → | 2 |
| even1(0) | → | 4 |
| even1(0) | → | 2 |
| False1 | → | 2 |
| odd1(0) | → | 1 |
| odd1(0) | → | 4 |
| True1 | → | 1 |
| True1 | → | 4 |
| False1 | → | 4 |