The rewrite relation of the following TRS is considered.
| 0(0(1(x1))) | → | 0(2(3(0(1(x1))))) | (1) |
| 0(0(1(x1))) | → | 0(4(0(5(4(1(x1)))))) | (2) |
| 0(0(1(x1))) | → | 2(1(0(0(3(4(x1)))))) | (3) |
| 0(0(1(x1))) | → | 4(0(5(4(0(1(x1)))))) | (4) |
| 0(1(0(x1))) | → | 0(0(2(1(2(x1))))) | (5) |
| 0(1(0(x1))) | → | 1(0(0(5(4(x1))))) | (6) |
| 0(1(0(x1))) | → | 0(0(2(5(4(1(x1)))))) | (7) |
| 0(1(1(x1))) | → | 1(0(3(4(1(x1))))) | (8) |
| 0(1(1(x1))) | → | 5(0(3(4(1(1(x1)))))) | (9) |
| 5(0(1(x1))) | → | 0(5(4(1(x1)))) | (10) |
| 5(0(1(x1))) | → | 2(5(4(0(1(x1))))) | (11) |
| 5(0(1(x1))) | → | 5(0(2(1(2(x1))))) | (12) |
| 5(0(1(x1))) | → | 0(1(4(5(4(4(x1)))))) | (13) |
| 5(0(1(x1))) | → | 0(5(4(1(4(4(x1)))))) | (14) |
| 5(0(1(x1))) | → | 5(0(4(3(0(1(x1)))))) | (15) |
| 5(1(0(x1))) | → | 5(0(2(2(1(x1))))) | (16) |
| 5(1(0(x1))) | → | 5(0(5(4(1(x1))))) | (17) |
| 5(1(0(x1))) | → | 0(5(0(2(2(1(x1)))))) | (18) |
| 5(1(0(x1))) | → | 1(4(0(5(2(3(x1)))))) | (19) |
| 5(1(0(x1))) | → | 1(5(0(4(4(2(x1)))))) | (20) |
| 5(1(0(x1))) | → | 4(4(1(0(4(5(x1)))))) | (21) |
| 5(1(1(x1))) | → | 1(1(5(4(x1)))) | (22) |
| 5(1(1(x1))) | → | 5(4(1(1(x1)))) | (23) |
| 5(1(1(x1))) | → | 1(5(3(4(1(x1))))) | (24) |
| 5(1(1(x1))) | → | 1(1(4(5(4(4(x1)))))) | (25) |
| 5(1(1(x1))) | → | 3(5(2(3(1(1(x1)))))) | (26) |
| 5(1(1(x1))) | → | 4(1(2(1(5(4(x1)))))) | (27) |
| 0(1(3(0(x1)))) | → | 0(2(0(2(1(3(x1)))))) | (28) |
| 0(1(5(0(x1)))) | → | 0(0(5(4(1(5(x1)))))) | (29) |
| 0(1(5(0(x1)))) | → | 0(5(4(2(1(0(x1)))))) | (30) |
| 0(3(0(1(x1)))) | → | 0(0(4(1(3(0(x1)))))) | (31) |
| 0(3(1(0(x1)))) | → | 0(0(2(3(1(x1))))) | (32) |
| 0(3(1(1(x1)))) | → | 5(1(1(0(3(4(x1)))))) | (33) |
| 5(0(1(0(x1)))) | → | 5(0(0(4(1(3(x1)))))) | (34) |
| 5(1(2(0(x1)))) | → | 1(4(0(5(4(2(x1)))))) | (35) |
| 5(1(2(0(x1)))) | → | 5(0(4(2(2(1(x1)))))) | (36) |
| 5(1(4(0(x1)))) | → | 1(5(4(0(2(3(x1)))))) | (37) |
| 5(1(4(0(x1)))) | → | 4(5(2(1(3(0(x1)))))) | (38) |
| 5(1(5(1(x1)))) | → | 5(4(1(5(1(x1))))) | (39) |
| 5(3(0(1(x1)))) | → | 0(1(5(2(3(x1))))) | (40) |
| 5(3(1(0(x1)))) | → | 1(4(3(5(0(x1))))) | (41) |
| 5(3(1(0(x1)))) | → | 1(5(0(4(3(x1))))) | (42) |
| 5(3(1(0(x1)))) | → | 5(4(3(1(0(x1))))) | (43) |
| 5(3(1(0(x1)))) | → | 1(3(0(4(3(5(x1)))))) | (44) |
| 5(3(1(1(x1)))) | → | 1(1(5(3(3(4(x1)))))) | (45) |
| 0(1(2(5(0(x1))))) | → | 1(5(4(0(2(0(x1)))))) | (46) |
| 0(1(4(2(0(x1))))) | → | 1(0(4(2(3(0(x1)))))) | (47) |
| 1(4(5(1(0(x1))))) | → | 5(4(2(1(1(0(x1)))))) | (48) |
| 5(0(1(4(0(x1))))) | → | 1(4(5(4(0(0(x1)))))) | (49) |
| 5(5(1(0(0(x1))))) | → | 5(5(0(4(1(0(x1)))))) | (50) |
There are 132 ruless (increase limit for explicit display).
The dependency pairs are split into 2 components.
| 0#(1(5(0(x1)))) | → | 5#(x1) | (123) |
| 5#(1(0(x1))) | → | 5#(x1) | (104) |
| 5#(3(1(0(x1)))) | → | 5#(0(x1)) | (158) |
| 5#(3(1(0(x1)))) | → | 5#(x1) | (165) |
| 5#(0(1(4(0(x1))))) | → | 0#(0(x1)) | (178) |
| 0#(3(0(1(x1)))) | → | 0#(x1) | (130) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| 5#(0(1(4(0(x1))))) | → | 0#(0(x1)) | (178) |
| 1 | > | 1 | |
| 0#(3(0(1(x1)))) | → | 0#(x1) | (130) |
| 1 | > | 1 | |
| 0#(1(5(0(x1)))) | → | 5#(x1) | (123) |
| 1 | > | 1 | |
| 5#(1(0(x1))) | → | 5#(x1) | (104) |
| 1 | > | 1 | |
| 5#(3(1(0(x1)))) | → | 5#(0(x1)) | (158) |
| 1 | > | 1 | |
| 5#(3(1(0(x1)))) | → | 5#(x1) | (165) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| 1#(4(5(1(0(x1))))) | → | 1#(1(0(x1))) | (175) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| 1#(4(5(1(0(x1))))) | → | 1#(1(0(x1))) | (175) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.