by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| q(0(x0)) | → | p(p(s(s(0(s(s(s(s(x0))))))))) |
| q(s(x0)) | → | p(p(s(s(s(s(s(s(r(p(p(s(s(x0))))))))))))) |
| r(0(x0)) | → | p(s(p(s(0(p(p(p(s(s(s(x0))))))))))) |
| r(s(x0)) | → | p(s(p(s(s(q(p(s(p(s(x0)))))))))) |
| p(p(s(x0))) | → | p(x0) |
| p(s(x0)) | → | x0 |
| p(0(x0)) | → | 0(s(s(s(x0)))) |
final states:
{40, 2, 39, 30, 22, 11, 1}
transitions:
| 18 | → | 11 |
| 18 | → | 56 |
| 3 | → | 41 |
| 3 | → | 12 |
| 3 | → | 48 |
| 50 | → | 1 |
| 37 | → | 30 |
| 31 | → | 33 |
| 1 | → | 34 |
| 40 | → | 39 |
| 8 | → | 49 |
| 8 | → | 10 |
| 26 | → | 28 |
| 22 | → | 14 |
| 2 | → | 31 |
| 2 | → | 13 |
| 2 | → | 42 |
| 2 | → | 39 |
| 11 | → | 34 |
| 4 | → | 47 |
| 4 | → | 23 |
| 28 | → | 22 |
| 7 | → | 50 |
| 30 | → | 14 |
| 42 | → | 13 |
| 42 | → | 25 |
| 35 | → | 37 |
| 48 | → | 24 |
| 19 | → | 55 |
| 19 | → | 21 |
| 56 | → | 11 |
| r0(13) | → | 14 |
| q0(33) | → | 34 |
| 00(6) | → | 7 |
| 00(25) | → | 26 |
| 00(5) | → | 40 |
| p1(47) | → | 48 |
| p1(41) | → | 42 |
| p1(49) | → | 50 |
| p1(55) | → | 56 |
| p0(9) | → | 10 |
| p0(3) | → | 31 |
| p0(5) | → | 23 |
| p0(23) | → | 24 |
| p0(24) | → | 25 |
| p0(29) | → | 22 |
| p0(38) | → | 30 |
| p0(10) | → | 1 |
| p0(2) | → | 39 |
| p0(4) | → | 12 |
| p0(27) | → | 28 |
| p0(20) | → | 21 |
| p0(12) | → | 13 |
| p0(36) | → | 37 |
| p0(32) | → | 33 |
| p0(21) | → | 11 |
| s0(2) | → | 3 |
| s0(18) | → | 19 |
| s0(28) | → | 29 |
| s0(19) | → | 20 |
| s0(4) | → | 5 |
| s0(8) | → | 9 |
| s0(26) | → | 27 |
| s0(37) | → | 38 |
| s0(3) | → | 4 |
| s0(17) | → | 18 |
| s0(14) | → | 15 |
| s0(7) | → | 8 |
| s0(15) | → | 16 |
| s0(35) | → | 36 |
| s0(34) | → | 35 |
| s0(16) | → | 17 |
| s0(31) | → | 32 |
| s0(5) | → | 6 |
| f50 | → | 2 |