The rewrite relation of the following TRS is considered.
| a__f(f(X)) | → | a__c(f(g(f(X)))) | (1) |
| a__c(X) | → | d(X) | (2) |
| a__h(X) | → | a__c(d(X)) | (3) |
| mark(f(X)) | → | a__f(mark(X)) | (4) |
| mark(c(X)) | → | a__c(X) | (5) |
| mark(h(X)) | → | a__h(mark(X)) | (6) |
| mark(g(X)) | → | g(X) | (7) |
| mark(d(X)) | → | d(X) | (8) |
| a__f(X) | → | f(X) | (9) |
| a__c(X) | → | c(X) | (10) |
| a__h(X) | → | h(X) | (11) |
final states:
{1, 2}
transitions:
| a__f0(2) | → | 1 |
| a__c0(2) | → | 1 |
| a__h0(2) | → | 1 |
| mark0(2) | → | 1 |
| f1(2) | → | 1 |
| d1(2) | → | 1 |
| c1(2) | → | 1 |
| h1(2) | → | 1 |
| a__c1(2) | → | 1 |
| g1(2) | → | 1 |
| d2(2) | → | 1 |
| c2(2) | → | 1 |
| a__c1(3) | → | 1 |
| d2(3) | → | 1 |
| c2(3) | → | 1 |
| a__c1(6) | → | 1 |
| d2(6) | → | 1 |
| c2(6) | → | 1 |
| a__f1(7) | → | 1 |
| f2(7) | → | 1 |
| a__h1(8) | → | 1 |
| h2(8) | → | 1 |
| a__c2(9) | → | 1 |
| d3(9) | → | 1 |
| c3(9) | → | 1 |
| a__c2(10) | → | 1 |
| d3(10) | → | 1 |
| c3(10) | → | 1 |
| f0(2) | → | 2 |
| g0(2) | → | 2 |
| d0(2) | → | 2 |
| c0(2) | → | 2 |
| h0(2) | → | 2 |
| f1(4) | → | 3 |
| g1(5) | → | 4 |
| f1(2) | → | 5 |
| d1(2) | → | 6 |
| mark1(2) | → | 7 |
| a__c1(2) | → | 7 |
| g1(2) | → | 7 |
| d1(2) | → | 7 |
| d2(2) | → | 7 |
| c2(2) | → | 7 |
| a__f1(7) | → | 7 |
| f2(7) | → | 7 |
| a__h1(8) | → | 7 |
| h2(8) | → | 7 |
| a__c2(9) | → | 7 |
| d3(9) | → | 7 |
| c3(9) | → | 7 |
| a__c2(10) | → | 7 |
| d3(10) | → | 7 |
| c3(10) | → | 7 |
| mark1(2) | → | 8 |
| a__c1(2) | → | 8 |
| g1(2) | → | 8 |
| d1(2) | → | 8 |
| d2(2) | → | 8 |
| c2(2) | → | 8 |
| a__f1(7) | → | 8 |
| f2(7) | → | 8 |
| a__h1(8) | → | 8 |
| h2(8) | → | 8 |
| a__c2(9) | → | 8 |
| d3(9) | → | 8 |
| c3(9) | → | 8 |
| a__c2(10) | → | 8 |
| d3(10) | → | 8 |
| c3(10) | → | 8 |
| d2(8) | → | 9 |
| f2(11) | → | 10 |
| g2(12) | → | 11 |
| f2(7) | → | 12 |