by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| a(a(b(a(a(b(a(x0))))))) | → | a(b(a(a(b(a(a(a(b(x0))))))))) |
| a(b(a(a(b(a(a(x0))))))) | → | b(a(a(a(b(a(a(b(a(x0))))))))) |
final states:
{1}
transitions:
| 33 | → | 119 |
| 128 | → | 82 |
| 98 | → | 85 |
| 1 | → | 8 |
| 1 | → | 5 |
| 1 | → | 3 |
| 1 | → | 32 |
| 1 | → | 52 |
| 40 | → | 27 |
| 8 | → | 21 |
| 60 | → | 24 |
| 38 | → | 80 |
| 36 | → | 89 |
| 88 | → | 10 |
| 4 | → | 51 |
| 7 | → | 31 |
| 30 | → | 9 |
| 30 | → | 22 |
| 30 | → | 6 |
| a2(124) | → | 125 |
| a2(126) | → | 127 |
| a2(91) | → | 92 |
| a2(125) | → | 126 |
| a2(95) | → | 96 |
| a2(92) | → | 93 |
| a2(121) | → | 122 |
| a2(96) | → | 97 |
| a2(94) | → | 95 |
| a2(119) | → | 120 |
| a2(122) | → | 123 |
| a2(89) | → | 90 |
| b0(3) | → | 4 |
| b0(6) | → | 7 |
| b0(10) | → | 1 |
| a0(5) | → | 6 |
| a0(7) | → | 8 |
| a0(9) | → | 10 |
| a0(8) | → | 9 |
| a0(2) | → | 3 |
| a0(4) | → | 5 |
| f20 | → | 2 |
| a1(28) | → | 29 |
| a1(37) | → | 38 |
| a1(51) | → | 52 |
| a1(23) | → | 24 |
| a1(24) | → | 25 |
| a1(26) | → | 27 |
| a1(54) | → | 55 |
| a1(58) | → | 59 |
| a1(86) | → | 87 |
| a1(57) | → | 58 |
| a1(38) | → | 39 |
| a1(82) | → | 83 |
| a1(81) | → | 82 |
| a1(53) | → | 54 |
| a1(84) | → | 85 |
| a1(85) | → | 86 |
| a1(31) | → | 32 |
| a1(34) | → | 35 |
| a1(27) | → | 28 |
| a1(33) | → | 34 |
| a1(56) | → | 57 |
| a1(36) | → | 37 |
| a1(21) | → | 22 |
| b2(123) | → | 124 |
| b2(90) | → | 91 |
| b2(93) | → | 94 |
| b2(127) | → | 128 |
| b2(120) | → | 121 |
| b2(97) | → | 98 |
| b1(22) | → | 23 |
| b1(29) | → | 30 |
| b1(80) | → | 81 |
| b1(55) | → | 56 |
| b1(87) | → | 88 |
| b1(35) | → | 36 |
| b1(59) | → | 60 |
| b1(32) | → | 33 |
| b1(52) | → | 53 |
| b1(39) | → | 40 |
| b1(83) | → | 84 |
| b1(25) | → | 26 |