by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| c(b(a(a(x0)))) | → | a(a(b(a(a(b(c(b(a(c(x0)))))))))) |
| a(a(b(c(x0)))) | → | c(a(b(c(b(a(a(b(a(a(x0)))))))))) |
final states:
{1}
transitions:
| 18 | → | 89 |
| 110 | → | 50 |
| 65 | → | 100 |
| 55 | → | 13 |
| 99 | → | 57 |
| 62 | → | 133 |
| 1 | → | 4 |
| 1 | → | 3 |
| 8 | → | 45 |
| 21 | → | 56 |
| 22 | → | 7 |
| 143 | → | 101 |
| 11 | → | 12 |
| 66 | → | 47 |
| b0(9) | → | 10 |
| b0(7) | → | 8 |
| b0(4) | → | 5 |
| b2(138) | → | 139 |
| b2(135) | → | 136 |
| b2(105) | → | 106 |
| b2(96) | → | 97 |
| b2(94) | → | 95 |
| b2(91) | → | 92 |
| b2(140) | → | 141 |
| b2(107) | → | 108 |
| b2(102) | → | 103 |
| c0(8) | → | 9 |
| c0(11) | → | 1 |
| a1(59) | → | 60 |
| a1(45) | → | 46 |
| a1(60) | → | 61 |
| a1(56) | → | 57 |
| a1(46) | → | 47 |
| a1(64) | → | 65 |
| a1(57) | → | 58 |
| a1(12) | → | 13 |
| a1(15) | → | 16 |
| a1(49) | → | 50 |
| a1(20) | → | 21 |
| a1(13) | → | 14 |
| a1(53) | → | 54 |
| a1(48) | → | 49 |
| a1(16) | → | 17 |
| b1(19) | → | 20 |
| b1(58) | → | 59 |
| b1(61) | → | 62 |
| b1(50) | → | 51 |
| b1(52) | → | 53 |
| b1(63) | → | 64 |
| b1(14) | → | 15 |
| b1(47) | → | 48 |
| b1(17) | → | 18 |
| c2(109) | → | 110 |
| c2(95) | → | 96 |
| c2(98) | → | 99 |
| c2(106) | → | 107 |
| c2(139) | → | 140 |
| c2(142) | → | 143 |
| c1(51) | → | 52 |
| c1(18) | → | 19 |
| c1(65) | → | 66 |
| c1(54) | → | 55 |
| c1(21) | → | 22 |
| c1(62) | → | 63 |
| f30 | → | 2 |
| a2(108) | → | 109 |
| a2(101) | → | 102 |
| a2(100) | → | 101 |
| a2(97) | → | 98 |
| a2(141) | → | 142 |
| a2(136) | → | 137 |
| a2(90) | → | 91 |
| a2(93) | → | 94 |
| a2(92) | → | 93 |
| a2(89) | → | 90 |
| a2(103) | → | 104 |
| a2(133) | → | 134 |
| a2(137) | → | 138 |
| a2(134) | → | 135 |
| a2(104) | → | 105 |
| a0(10) | → | 11 |
| a0(6) | → | 7 |
| a0(5) | → | 6 |
| a0(2) | → | 3 |
| a0(3) | → | 4 |