The rewrite relation of the following TRS is considered.
| 2(7(x1)) | → | 1(8(x1)) | (1) |
| 2(8(1(x1))) | → | 8(x1) | (2) |
| 2(8(x1)) | → | 4(x1) | (3) |
| 5(9(x1)) | → | 0(x1) | (4) |
| 4(x1) | → | 5(2(3(x1))) | (5) |
| 5(3(x1)) | → | 6(0(x1)) | (6) |
| 2(8(x1)) | → | 7(x1) | (7) |
| 4(7(x1)) | → | 1(3(x1)) | (8) |
| 5(2(6(x1))) | → | 6(2(4(x1))) | (9) |
| 9(7(x1)) | → | 7(5(x1)) | (10) |
| 7(2(x1)) | → | 4(x1) | (11) |
| 7(0(x1)) | → | 9(3(x1)) | (12) |
| 6(9(x1)) | → | 9(x1) | (13) |
| 9(5(9(x1))) | → | 5(7(x1)) | (14) |
| 4(x1) | → | 9(6(6(x1))) | (15) |
| 9(x1) | → | 6(7(x1)) | (16) |
| 6(2(x1)) | → | 7(7(x1)) | (17) |
| 2(4(x1)) | → | 0(7(x1)) | (18) |
| 6(6(x1)) | → | 3(x1) | (19) |
| 0(3(x1)) | → | 5(3(x1)) | (20) |
| [4(x1)] | = |
|
||||||||||||||||||||||||
| [3(x1)] | = |
|
||||||||||||||||||||||||
| [2(x1)] | = |
|
||||||||||||||||||||||||
| [1(x1)] | = |
|
||||||||||||||||||||||||
| [9(x1)] | = |
|
||||||||||||||||||||||||
| [7(x1)] | = |
|
||||||||||||||||||||||||
| [0(x1)] | = |
|
||||||||||||||||||||||||
| [6(x1)] | = |
|
||||||||||||||||||||||||
| [5(x1)] | = |
|
||||||||||||||||||||||||
| [8(x1)] | = |
|
| 2(8(1(x1))) | → | 8(x1) | (2) |
| 2(8(x1)) | → | 4(x1) | (3) |
| 2(8(x1)) | → | 7(x1) | (7) |
| [4(x1)] | = |
|
||||||||||||||||||||||||
| [3(x1)] | = |
|
||||||||||||||||||||||||
| [2(x1)] | = |
|
||||||||||||||||||||||||
| [1(x1)] | = |
|
||||||||||||||||||||||||
| [9(x1)] | = |
|
||||||||||||||||||||||||
| [7(x1)] | = |
|
||||||||||||||||||||||||
| [0(x1)] | = |
|
||||||||||||||||||||||||
| [6(x1)] | = |
|
||||||||||||||||||||||||
| [5(x1)] | = |
|
||||||||||||||||||||||||
| [8(x1)] | = |
|
| 5(2(6(x1))) | → | 6(2(4(x1))) | (9) |
| [4(x1)] | = | 1 · x1 + -∞ |
| [3(x1)] | = | 0 · x1 + -∞ |
| [2(x1)] | = | 1 · x1 + -∞ |
| [1(x1)] | = | 1 · x1 + -∞ |
| [9(x1)] | = | 0 · x1 + -∞ |
| [7(x1)] | = | 0 · x1 + -∞ |
| [0(x1)] | = | 0 · x1 + -∞ |
| [6(x1)] | = | 0 · x1 + -∞ |
| [5(x1)] | = | 0 · x1 + -∞ |
| [8(x1)] | = | 0 · x1 + -∞ |
| 4(x1) | → | 9(6(6(x1))) | (15) |
| 6(2(x1)) | → | 7(7(x1)) | (17) |
| 2(4(x1)) | → | 0(7(x1)) | (18) |
| 5#(9(x1)) | → | 0#(x1) | (21) |
| 4#(x1) | → | 2#(3(x1)) | (22) |
| 4#(x1) | → | 5#(2(3(x1))) | (23) |
| 5#(3(x1)) | → | 0#(x1) | (24) |
| 5#(3(x1)) | → | 6#(0(x1)) | (25) |
| 9#(7(x1)) | → | 5#(x1) | (26) |
| 9#(7(x1)) | → | 7#(5(x1)) | (27) |
| 7#(2(x1)) | → | 4#(x1) | (28) |
| 7#(0(x1)) | → | 9#(3(x1)) | (29) |
| 9#(5(9(x1))) | → | 7#(x1) | (30) |
| 9#(5(9(x1))) | → | 5#(7(x1)) | (31) |
| 9#(x1) | → | 7#(x1) | (32) |
| 9#(x1) | → | 6#(7(x1)) | (33) |
| 0#(3(x1)) | → | 5#(3(x1)) | (34) |
The dependency pairs are split into 2 components.
| 5#(3(x1)) | → | 0#(x1) | (24) |
| 0#(3(x1)) | → | 5#(3(x1)) | (34) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| 5#(3(x1)) | → | 0#(x1) | (24) |
| 1 | > | 1 | |
| 0#(3(x1)) | → | 5#(3(x1)) | (34) |
| 1 | ≥ | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| 7#(0(x1)) | → | 9#(3(x1)) | (29) |
| 9#(x1) | → | 7#(x1) | (32) |
| π(7#) | = | { 1 } |
| π(9#) | = | { 1 } |
| π(3) | = | { 1 } |
| 7#(0(x1)) | → | 9#(3(x1)) | (29) |
The dependency pairs are split into 0 components.