The rewrite relation of the following TRS is considered.
| @(Cons(x,xs),ys) | → | Cons(x,@(xs,ys)) | (1) |
| @(Nil,ys) | → | ys | (2) |
| game(p1,Cons(x',xs'),Cons(Capture,xs)) | → | game(Cons(x',p1),xs',xs) | (3) |
| game(p1,p2,Cons(Swap,xs)) | → | game(p2,p1,xs) | (4) |
| equal(Capture,Capture) | → | True | (5) |
| equal(Capture,Swap) | → | False | (6) |
| equal(Swap,Capture) | → | False | (7) |
| equal(Swap,Swap) | → | True | (8) |
| game(p1,p2,Nil) | → | @(p1,p2) | (9) |
| goal(p1,p2,moves) | → | game(p1,p2,moves) | (10) |
final states:
{0, 1, 2, 3, 4}
transitions:
| Cons0(0,0) | → | 0 |
| Nil0 | → | 0 |
| Capture0 | → | 0 |
| Swap0 | → | 0 |
| True0 | → | 0 |
| False0 | → | 0 |
| @0(0,0) | → | 1 |
| game0(0,0,0) | → | 2 |
| equal0(0,0) | → | 3 |
| goal0(0,0,0) | → | 4 |
| @1(0,0) | → | 5 |
| Cons1(0,5) | → | 1 |
| Cons1(0,0) | → | 6 |
| game1(6,0,0) | → | 2 |
| game1(0,0,0) | → | 2 |
| True1 | → | 3 |
| False1 | → | 3 |
| @1(0,0) | → | 2 |
| game1(0,0,0) | → | 4 |
| Cons1(0,5) | → | 2 |
| Cons1(0,5) | → | 5 |
| Cons1(0,6) | → | 6 |
| game1(6,0,0) | → | 4 |
| game1(0,6,0) | → | 2 |
| @1(6,0) | → | 2 |
| @1(0,0) | → | 4 |
| Cons1(0,5) | → | 4 |
| @2(0,0) | → | 7 |
| Cons2(0,7) | → | 2 |
| @2(6,0) | → | 7 |
| game1(6,6,0) | → | 2 |
| game1(0,6,0) | → | 4 |
| @1(0,6) | → | 2 |
| @1(6,0) | → | 4 |
| @1(0,6) | → | 5 |
| Cons2(0,7) | → | 4 |
| game1(6,6,0) | → | 4 |
| @1(6,6) | → | 2 |
| @1(0,6) | → | 4 |
| Cons1(0,5) | → | 7 |
| Cons2(0,7) | → | 7 |
| @2(0,6) | → | 7 |
| @2(6,6) | → | 7 |
| @1(6,6) | → | 4 |
| 0 | → | 1 |
| 0 | → | 2 |
| 0 | → | 5 |
| 0 | → | 4 |
| 0 | → | 7 |
| 6 | → | 2 |
| 6 | → | 4 |
| 6 | → | 5 |
| 6 | → | 7 |