The rewrite relation of the following TRS is considered.
| f(b(a,z)) | → | z | (1) |
| b(y,b(a,z)) | → | b(f(c(y,y,a)),b(f(z),a)) | (2) |
| f(f(f(c(z,x,a)))) | → | b(f(x),z) | (3) |
final states:
{5}
transitions:
| 5 | → | 7 |
| 5 | → | 12 |
| a2 | → | 11 |
| a3 | → | 21 |
| c3(15,15,21) | → | 24 |
| f3(11) | → | 22 |
| f3(24) | → | 25 |
| c1(5,5,6) | → | 9 |
| a1 | → | 6 |
| f1(9) | → | 10 |
| f1(5) | → | 7 |
| f0(5) | → | 5 |
| b0(5,5) | → | 5 |
| b2(12,11) | → | 13 |
| b2(15,13) | → | 5 |
| f2(5) | → | 12 |
| f2(6) | → | 12 |
| f2(14) | → | 15 |
| c0(5,5,5) | → | 5 |
| b1(7,6) | → | 8 |
| b1(10,8) | → | 5 |
| b1(7,5) | → | 5 |
| b3(22,21) | → | 23 |
| b3(25,23) | → | 12 |
| b3(25,23) | → | 7 |
| b3(25,23) | → | 5 |
| c2(7,7,11) | → | 14 |
| c2(10,10,11) | → | 14 |
| a0 | → | 5 |