The rewrite relation of the following TRS is considered.
0(1(0(1(x1)))) | → | 0(1(1(1(0(0(1(2(2(2(x1)))))))))) | (1) |
0(3(4(4(x1)))) | → | 0(0(0(3(1(1(4(2(2(0(x1)))))))))) | (2) |
1(5(1(5(4(x1))))) | → | 1(0(0(2(2(0(5(2(2(4(x1)))))))))) | (3) |
3(4(5(3(4(x1))))) | → | 3(5(0(2(1(1(1(2(1(4(x1)))))))))) | (4) |
4(3(4(3(4(x1))))) | → | 2(1(1(1(4(1(2(4(2(0(x1)))))))))) | (5) |
5(0(1(0(1(x1))))) | → | 5(0(2(0(1(1(4(2(1(2(x1)))))))))) | (6) |
1(0(1(0(1(4(x1)))))) | → | 1(0(2(4(5(4(2(4(2(4(x1)))))))))) | (7) |
1(1(3(4(1(5(x1)))))) | → | 1(1(0(0(2(2(5(2(0(0(x1)))))))))) | (8) |
1(3(1(1(3(3(x1)))))) | → | 1(2(4(2(0(2(1(0(2(5(x1)))))))))) | (9) |
1(3(1(5(2(3(x1)))))) | → | 1(4(3(2(1(0(0(2(4(3(x1)))))))))) | (10) |
1(5(0(5(5(3(x1)))))) | → | 2(1(1(1(1(2(1(3(5(3(x1)))))))))) | (11) |
2(1(3(1(5(5(x1)))))) | → | 1(1(2(2(0(5(0(0(2(2(x1)))))))))) | (12) |
2(2(4(3(4(5(x1)))))) | → | 2(0(1(4(0(0(2(0(0(0(x1)))))))))) | (13) |
2(3(1(0(3(4(x1)))))) | → | 0(0(1(1(5(2(4(1(1(4(x1)))))))))) | (14) |
2(3(3(4(1(5(x1)))))) | → | 0(0(2(4(4(2(0(4(1(3(x1)))))))))) | (15) |
2(5(0(5(5(1(x1)))))) | → | 3(0(1(4(4(0(0(0(0(1(x1)))))))))) | (16) |
3(0(4(3(3(4(x1)))))) | → | 2(3(0(3(5(1(2(4(2(4(x1)))))))))) | (17) |
3(2(3(3(0(4(x1)))))) | → | 5(4(2(2(0(0(4(2(4(4(x1)))))))))) | (18) |
3(3(5(4(3(4(x1)))))) | → | 0(5(1(1(0(4(0(2(4(4(x1)))))))))) | (19) |
3(5(4(2(1(0(x1)))))) | → | 2(5(0(0(0(0(0(4(4(0(x1)))))))))) | (20) |
4(1(3(4(3(1(x1)))))) | → | 4(2(5(0(1(0(0(0(4(4(x1)))))))))) | (21) |
4(2(1(0(2(5(x1)))))) | → | 4(2(5(4(2(2(2(4(2(5(x1)))))))))) | (22) |
4(3(3(5(1(1(x1)))))) | → | 4(4(2(4(4(2(5(0(1(2(x1)))))))))) | (23) |
5(4(0(1(3(0(x1)))))) | → | 0(2(4(2(2(1(2(0(0(0(x1)))))))))) | (24) |
0(4(1(5(5(3(5(x1))))))) | → | 0(2(2(0(1(2(5(2(5(0(x1)))))))))) | (25) |
0(4(4(3(4(1(3(x1))))))) | → | 0(4(2(4(1(3(2(0(2(2(x1)))))))))) | (26) |
1(3(3(4(5(2(5(x1))))))) | → | 1(1(1(4(5(1(2(5(2(4(x1)))))))))) | (27) |
1(5(2(5(1(5(2(x1))))))) | → | 1(2(3(0(2(3(0(1(0(2(x1)))))))))) | (28) |
1(5(3(2(4(5(4(x1))))))) | → | 1(1(0(3(0(0(0(0(3(4(x1)))))))))) | (29) |
1(5(5(5(3(2(1(x1))))))) | → | 1(4(1(4(2(1(3(0(1(1(x1)))))))))) | (30) |
2(1(2(3(1(3(3(x1))))))) | → | 2(1(4(1(5(1(1(1(1(1(x1)))))))))) | (31) |
3(0(2(1(3(2(1(x1))))))) | → | 1(2(0(0(3(3(4(2(2(1(x1)))))))))) | (32) |
3(0(4(4(3(4(5(x1))))))) | → | 1(2(2(4(3(2(2(2(0(4(x1)))))))))) | (33) |
3(1(3(1(5(4(1(x1))))))) | → | 0(1(2(2(5(5(5(4(2(0(x1)))))))))) | (34) |
3(2(5(2(1(3(4(x1))))))) | → | 0(2(1(3(1(2(1(4(2(2(x1)))))))))) | (35) |
3(3(1(3(1(3(3(x1))))))) | → | 1(2(1(3(0(5(5(1(2(1(x1)))))))))) | (36) |
3(3(1(5(0(3(4(x1))))))) | → | 2(0(0(5(1(2(1(4(1(4(x1)))))))))) | (37) |
3(3(3(5(2(4(5(x1))))))) | → | 3(1(0(0(1(4(2(2(0(5(x1)))))))))) | (38) |
3(4(3(3(4(3(5(x1))))))) | → | 5(1(1(1(1(1(4(2(3(3(x1)))))))))) | (39) |
3(4(3(4(4(3(2(x1))))))) | → | 2(5(4(5(3(4(2(4(4(0(x1)))))))))) | (40) |
4(1(3(4(1(0(2(x1))))))) | → | 4(4(1(5(1(2(1(4(2(2(x1)))))))))) | (41) |
4(5(0(4(1(3(1(x1))))))) | → | 1(1(1(2(0(0(4(4(5(1(x1)))))))))) | (42) |
4(5(0(5(3(2(1(x1))))))) | → | 1(1(4(1(3(0(2(4(2(1(x1)))))))))) | (43) |
4(5(0(5(3(4(5(x1))))))) | → | 1(1(1(0(5(4(0(2(4(5(x1)))))))))) | (44) |
4(5(3(1(4(4(3(x1))))))) | → | 4(5(5(5(4(2(4(4(2(3(x1)))))))))) | (45) |
4(5(3(4(1(4(5(x1))))))) | → | 4(5(4(0(2(0(1(2(1(0(x1)))))))))) | (46) |
4(5(4(3(4(1(0(x1))))))) | → | 1(4(1(1(2(4(0(1(2(0(x1)))))))))) | (47) |
5(3(2(1(5(3(4(x1))))))) | → | 5(1(2(1(3(3(5(1(2(4(x1)))))))))) | (48) |
5(3(4(3(1(3(3(x1))))))) | → | 5(1(1(4(2(4(3(3(4(3(x1)))))))))) | (49) |
5(3(4(4(3(1(2(x1))))))) | → | 5(1(0(5(0(3(5(1(1(1(x1)))))))))) | (50) |
5(4(3(2(3(1(3(x1))))))) | → | 0(0(0(2(3(0(2(5(4(3(x1)))))))))) | (51) |
5(4(3(4(3(1(5(x1))))))) | → | 0(2(0(0(0(0(4(1(5(0(x1)))))))))) | (52) |
5(5(3(3(3(5(4(x1))))))) | → | 0(3(5(2(2(1(0(4(2(2(x1)))))))))) | (53) |
5(5(4(5(3(5(5(x1))))))) | → | 5(2(4(2(2(2(4(1(5(2(x1)))))))))) | (54) |
0(4(3(4(3(1(x1)))))) | → | 2(5(0(3(0(2(2(4(0(0(x1)))))))))) | (55) |
2(3(2(5(5(3(x1)))))) | → | 0(0(2(3(1(2(2(1(0(4(x1)))))))))) | (56) |
5(0(1(5(1(5(x1)))))) | → | 5(0(1(4(0(1(1(0(0(2(x1)))))))))) | (57) |
1(3(1(3(5(4(1(x1))))))) | → | 1(0(4(0(0(5(1(0(5(4(x1)))))))))) | (58) |
3(3(2(4(5(1(2(x1))))))) | → | 5(1(1(5(1(4(1(2(2(2(x1)))))))))) | (59) |
4(4(5(3(1(1(0(x1))))))) | → | 4(0(5(0(1(2(2(2(0(2(x1)))))))))) | (60) |
{5(☐), 4(☐), 3(☐), 2(☐), 1(☐), 0(☐)}
We obtain the transformed TRSThere are 360 ruless (increase limit for explicit display).
As carrier we take the set {0,...,5}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 6):
[5(x1)] | = | 6x1 + 0 |
[4(x1)] | = | 6x1 + 1 |
[3(x1)] | = | 6x1 + 2 |
[2(x1)] | = | 6x1 + 3 |
[1(x1)] | = | 6x1 + 4 |
[0(x1)] | = | 6x1 + 5 |
There are 2160 ruless (increase limit for explicit display).
[50(x1)] | = |
x1 +
|
||||
[51(x1)] | = |
x1 +
|
||||
[52(x1)] | = |
x1 +
|
||||
[53(x1)] | = |
x1 +
|
||||
[54(x1)] | = |
x1 +
|
||||
[55(x1)] | = |
x1 +
|
||||
[40(x1)] | = |
x1 +
|
||||
[41(x1)] | = |
x1 +
|
||||
[42(x1)] | = |
x1 +
|
||||
[43(x1)] | = |
x1 +
|
||||
[44(x1)] | = |
x1 +
|
||||
[45(x1)] | = |
x1 +
|
||||
[30(x1)] | = |
x1 +
|
||||
[31(x1)] | = |
x1 +
|
||||
[32(x1)] | = |
x1 +
|
||||
[33(x1)] | = |
x1 +
|
||||
[34(x1)] | = |
x1 +
|
||||
[35(x1)] | = |
x1 +
|
||||
[20(x1)] | = |
x1 +
|
||||
[21(x1)] | = |
x1 +
|
||||
[22(x1)] | = |
x1 +
|
||||
[23(x1)] | = |
x1 +
|
||||
[24(x1)] | = |
x1 +
|
||||
[25(x1)] | = |
x1 +
|
||||
[10(x1)] | = |
x1 +
|
||||
[11(x1)] | = |
x1 +
|
||||
[12(x1)] | = |
x1 +
|
||||
[13(x1)] | = |
x1 +
|
||||
[14(x1)] | = |
x1 +
|
||||
[15(x1)] | = |
x1 +
|
||||
[00(x1)] | = |
x1 +
|
||||
[01(x1)] | = |
x1 +
|
||||
[02(x1)] | = |
x1 +
|
||||
[03(x1)] | = |
x1 +
|
||||
[04(x1)] | = |
x1 +
|
||||
[05(x1)] | = |
x1 +
|
There are 2148 ruless (increase limit for explicit display).
14(04(15(04(05(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(05(x1))))))))))) | (2581) |
13(04(15(04(05(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(05(x1))))))))))) | (2582) |
14(04(15(04(15(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(15(x1))))))))))) | (2583) |
13(04(15(04(15(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(15(x1))))))))))) | (2584) |
14(04(15(04(25(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(25(x1))))))))))) | (2585) |
13(04(15(04(25(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(25(x1))))))))))) | (2586) |
14(04(15(04(35(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(35(x1))))))))))) | (2587) |
13(04(15(04(35(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(35(x1))))))))))) | (2588) |
14(04(15(04(45(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(45(x1))))))))))) | (2589) |
13(04(15(04(45(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(45(x1))))))))))) | (2590) |
14(04(15(04(55(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(55(x1))))))))))) | (2591) |
13(04(15(04(55(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(55(x1))))))))))) | (2592) |
13#(04(15(04(55(x1))))) | → | 13#(04(05(15(14(14(04(55(x1)))))))) | (2593) |
13#(04(15(04(55(x1))))) | → | 14#(14(04(55(x1)))) | (2594) |
13#(04(15(04(55(x1))))) | → | 14#(04(55(x1))) | (2595) |
13#(04(15(04(45(x1))))) | → | 13#(04(05(15(14(14(04(45(x1)))))))) | (2596) |
13#(04(15(04(45(x1))))) | → | 14#(14(04(45(x1)))) | (2597) |
13#(04(15(04(45(x1))))) | → | 14#(04(45(x1))) | (2598) |
13#(04(15(04(35(x1))))) | → | 13#(04(05(15(14(14(04(35(x1)))))))) | (2599) |
13#(04(15(04(35(x1))))) | → | 14#(14(04(35(x1)))) | (2600) |
13#(04(15(04(35(x1))))) | → | 14#(04(35(x1))) | (2601) |
13#(04(15(04(25(x1))))) | → | 13#(04(05(15(14(14(04(25(x1)))))))) | (2602) |
13#(04(15(04(25(x1))))) | → | 14#(14(04(25(x1)))) | (2603) |
13#(04(15(04(25(x1))))) | → | 14#(04(25(x1))) | (2604) |
13#(04(15(04(15(x1))))) | → | 13#(04(05(15(14(14(04(15(x1)))))))) | (2605) |
13#(04(15(04(15(x1))))) | → | 14#(14(04(15(x1)))) | (2606) |
13#(04(15(04(15(x1))))) | → | 14#(04(15(x1))) | (2607) |
13#(04(15(04(05(x1))))) | → | 13#(04(05(15(14(14(04(05(x1)))))))) | (2608) |
13#(04(15(04(05(x1))))) | → | 14#(14(04(05(x1)))) | (2609) |
13#(04(15(04(05(x1))))) | → | 14#(04(05(x1))) | (2610) |
14#(04(15(04(55(x1))))) | → | 13#(04(05(15(14(14(04(55(x1)))))))) | (2611) |
14#(04(15(04(55(x1))))) | → | 14#(14(04(55(x1)))) | (2612) |
14#(04(15(04(55(x1))))) | → | 14#(04(55(x1))) | (2613) |
14#(04(15(04(45(x1))))) | → | 13#(04(05(15(14(14(04(45(x1)))))))) | (2614) |
14#(04(15(04(45(x1))))) | → | 14#(14(04(45(x1)))) | (2615) |
14#(04(15(04(45(x1))))) | → | 14#(04(45(x1))) | (2616) |
14#(04(15(04(35(x1))))) | → | 13#(04(05(15(14(14(04(35(x1)))))))) | (2617) |
14#(04(15(04(35(x1))))) | → | 14#(14(04(35(x1)))) | (2618) |
14#(04(15(04(35(x1))))) | → | 14#(04(35(x1))) | (2619) |
14#(04(15(04(25(x1))))) | → | 13#(04(05(15(14(14(04(25(x1)))))))) | (2620) |
14#(04(15(04(25(x1))))) | → | 14#(14(04(25(x1)))) | (2621) |
14#(04(15(04(25(x1))))) | → | 14#(04(25(x1))) | (2622) |
14#(04(15(04(15(x1))))) | → | 13#(04(05(15(14(14(04(15(x1)))))))) | (2623) |
14#(04(15(04(15(x1))))) | → | 14#(14(04(15(x1)))) | (2624) |
14#(04(15(04(15(x1))))) | → | 14#(04(15(x1))) | (2625) |
14#(04(15(04(05(x1))))) | → | 13#(04(05(15(14(14(04(05(x1)))))))) | (2626) |
14#(04(15(04(05(x1))))) | → | 14#(14(04(05(x1)))) | (2627) |
14#(04(15(04(05(x1))))) | → | 14#(04(05(x1))) | (2628) |
[55(x1)] | = |
x1 +
|
||||
[45(x1)] | = |
x1 +
|
||||
[35(x1)] | = |
x1 +
|
||||
[23(x1)] | = |
x1 +
|
||||
[24(x1)] | = |
x1 +
|
||||
[25(x1)] | = |
x1 +
|
||||
[13(x1)] | = |
x1 +
|
||||
[14(x1)] | = |
x1 +
|
||||
[15(x1)] | = |
x1 +
|
||||
[04(x1)] | = |
x1 +
|
||||
[05(x1)] | = |
x1 +
|
||||
[13#(x1)] | = |
x1 +
|
||||
[14#(x1)] | = |
x1 +
|
14(04(15(04(05(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(05(x1))))))))))) | (2581) |
13(04(15(04(05(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(05(x1))))))))))) | (2582) |
14(04(15(04(15(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(15(x1))))))))))) | (2583) |
13(04(15(04(15(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(15(x1))))))))))) | (2584) |
14(04(15(04(25(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(25(x1))))))))))) | (2585) |
13(04(15(04(25(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(25(x1))))))))))) | (2586) |
14(04(15(04(35(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(35(x1))))))))))) | (2587) |
13(04(15(04(35(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(35(x1))))))))))) | (2588) |
14(04(15(04(45(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(45(x1))))))))))) | (2589) |
13(04(15(04(45(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(45(x1))))))))))) | (2590) |
14(04(15(04(55(x1))))) | → | 24(23(23(13(04(05(15(14(14(04(55(x1))))))))))) | (2591) |
13(04(15(04(55(x1))))) | → | 23(23(23(13(04(05(15(14(14(04(55(x1))))))))))) | (2592) |
13#(04(15(04(55(x1))))) | → | 14#(14(04(55(x1)))) | (2594) |
13#(04(15(04(55(x1))))) | → | 14#(04(55(x1))) | (2595) |
13#(04(15(04(45(x1))))) | → | 14#(14(04(45(x1)))) | (2597) |
13#(04(15(04(45(x1))))) | → | 14#(04(45(x1))) | (2598) |
13#(04(15(04(35(x1))))) | → | 14#(14(04(35(x1)))) | (2600) |
13#(04(15(04(35(x1))))) | → | 14#(04(35(x1))) | (2601) |
13#(04(15(04(25(x1))))) | → | 14#(14(04(25(x1)))) | (2603) |
13#(04(15(04(25(x1))))) | → | 14#(04(25(x1))) | (2604) |
13#(04(15(04(15(x1))))) | → | 14#(14(04(15(x1)))) | (2606) |
13#(04(15(04(15(x1))))) | → | 14#(04(15(x1))) | (2607) |
13#(04(15(04(05(x1))))) | → | 14#(14(04(05(x1)))) | (2609) |
13#(04(15(04(05(x1))))) | → | 14#(04(05(x1))) | (2610) |
14#(04(15(04(55(x1))))) | → | 13#(04(05(15(14(14(04(55(x1)))))))) | (2611) |
14#(04(15(04(55(x1))))) | → | 14#(14(04(55(x1)))) | (2612) |
14#(04(15(04(55(x1))))) | → | 14#(04(55(x1))) | (2613) |
14#(04(15(04(45(x1))))) | → | 13#(04(05(15(14(14(04(45(x1)))))))) | (2614) |
14#(04(15(04(45(x1))))) | → | 14#(14(04(45(x1)))) | (2615) |
14#(04(15(04(45(x1))))) | → | 14#(04(45(x1))) | (2616) |
14#(04(15(04(35(x1))))) | → | 13#(04(05(15(14(14(04(35(x1)))))))) | (2617) |
14#(04(15(04(35(x1))))) | → | 14#(14(04(35(x1)))) | (2618) |
14#(04(15(04(35(x1))))) | → | 14#(04(35(x1))) | (2619) |
14#(04(15(04(25(x1))))) | → | 13#(04(05(15(14(14(04(25(x1)))))))) | (2620) |
14#(04(15(04(25(x1))))) | → | 14#(14(04(25(x1)))) | (2621) |
14#(04(15(04(25(x1))))) | → | 14#(04(25(x1))) | (2622) |
14#(04(15(04(15(x1))))) | → | 13#(04(05(15(14(14(04(15(x1)))))))) | (2623) |
14#(04(15(04(15(x1))))) | → | 14#(14(04(15(x1)))) | (2624) |
14#(04(15(04(15(x1))))) | → | 14#(04(15(x1))) | (2625) |
14#(04(15(04(05(x1))))) | → | 13#(04(05(15(14(14(04(05(x1)))))))) | (2626) |
14#(04(15(04(05(x1))))) | → | 14#(14(04(05(x1)))) | (2627) |
14#(04(15(04(05(x1))))) | → | 14#(04(05(x1))) | (2628) |
The dependency pairs are split into 0 components.