The rewrite relation of the following TRS is considered.
| f(g(i(a,b,b'),c),d) | → | if(e,f(.(b,c),d'),f(.(b',c),d')) | (1) |
| f(g(h(a,b),c),d) | → | if(e,f(.(b,g(h(a,b),c)),d),f(c,d')) | (2) |
final states:
{0, 1}
transitions:
| g0(0,0) | → | 0 |
| i0(0,0,0) | → | 0 |
| a0 | → | 0 |
| b0 | → | 0 |
| b'0 | → | 0 |
| c0 | → | 0 |
| d0 | → | 0 |
| if0(0,0,0) | → | 0 |
| e0 | → | 0 |
| .0(0,0) | → | 0 |
| d'0 | → | 0 |
| h0(0,0) | → | 0 |
| f0(0,0) | → | 1 |
| e1 | → | 2 |
| b1 | → | 5 |
| c1 | → | 6 |
| .1(5,6) | → | 4 |
| d'1 | → | 7 |
| f1(4,7) | → | 3 |
| b'1 | → | 10 |
| .1(10,6) | → | 9 |
| f1(9,7) | → | 8 |
| if1(2,3,8) | → | 1 |
| a1 | → | 15 |
| b1 | → | 16 |
| h1(15,16) | → | 14 |
| c1 | → | 17 |
| g1(14,17) | → | 13 |
| .1(5,13) | → | 12 |
| d1 | → | 18 |
| f1(12,18) | → | 11 |
| c1 | → | 20 |
| f1(20,7) | → | 19 |
| if1(2,11,19) | → | 1 |