The rewrite relation of the following TRS is considered.
| a__c | → | a__f(g(c)) | (1) |
| a__f(g(X)) | → | g(X) | (2) |
| mark(c) | → | a__c | (3) |
| mark(f(X)) | → | a__f(X) | (4) |
| mark(g(X)) | → | g(X) | (5) |
| a__c | → | c | (6) |
| a__f(X) | → | f(X) | (7) |
final states:
{0, 1, 2, 3, 4, 5}
transitions:
| a__c0 | → | 0 |
| a__f0(0) | → | 1 |
| a__f0(1) | → | 1 |
| a__f0(2) | → | 1 |
| a__f0(3) | → | 1 |
| a__f0(4) | → | 1 |
| a__f0(5) | → | 1 |
| g0(0) | → | 2 |
| g0(1) | → | 2 |
| g0(2) | → | 2 |
| g0(3) | → | 2 |
| g0(4) | → | 2 |
| g0(5) | → | 2 |
| c0 | → | 3 |
| mark0(0) | → | 4 |
| mark0(1) | → | 4 |
| mark0(2) | → | 4 |
| mark0(3) | → | 4 |
| mark0(4) | → | 4 |
| mark0(5) | → | 4 |
| f0(0) | → | 5 |
| f0(1) | → | 5 |
| f0(2) | → | 5 |
| f0(3) | → | 5 |
| f0(4) | → | 5 |
| f0(5) | → | 5 |
| c1 | → | 7 |
| g1(7) | → | 6 |
| a__f1(6) | → | 0 |
| g1(0) | → | 1 |
| g1(1) | → | 1 |
| g1(2) | → | 1 |
| g1(3) | → | 1 |
| g1(4) | → | 1 |
| g1(5) | → | 1 |
| a__c1 | → | 4 |
| a__f1(0) | → | 4 |
| a__f1(1) | → | 4 |
| a__f1(2) | → | 4 |
| a__f1(3) | → | 4 |
| a__f1(4) | → | 4 |
| a__f1(5) | → | 4 |
| f1(0) | → | 1 |
| f1(1) | → | 1 |
| f1(2) | → | 1 |
| f1(3) | → | 1 |
| f1(4) | → | 1 |
| f1(5) | → | 1 |
| c2 | → | 9 |
| g2(9) | → | 8 |
| a__f2(8) | → | 1 |
| g2(7) | → | 0 |
| g2(0) | → | 1 |
| g2(1) | → | 1 |
| g2(2) | → | 1 |
| g2(3) | → | 1 |
| g2(4) | → | 1 |
| g2(5) | → | 1 |
| f2(6) | → | 0 |
| f2(0) | → | 1 |
| f2(1) | → | 1 |
| f2(2) | → | 1 |
| f2(3) | → | 1 |
| f2(4) | → | 1 |
| f2(5) | → | 1 |
| g3(9) | → | 1 |
| f3(8) | → | 0 |
| a__f1(8) | → | 0 |
| f2(8) | → | 0 |
| 1 | → | 4 |
| 7 | → | 0 |
| 9 | → | 1 |
| 0 | → | 1 |
| 8 | → | 0 |