The rewrite relation of the following TRS is considered.
a(b(x1)) | → | x1 | (1) |
a(c(x1)) | → | c(c(b(c(x1)))) | (2) |
b(c(x1)) | → | a(b(x1)) | (3) |
{c(☐), b(☐), a(☐)}
We obtain the transformed TRSc(a(b(x1))) | → | c(x1) | (4) |
c(a(c(x1))) | → | c(c(c(b(c(x1))))) | (5) |
c(b(c(x1))) | → | c(a(b(x1))) | (6) |
b(a(b(x1))) | → | b(x1) | (7) |
b(a(c(x1))) | → | b(c(c(b(c(x1))))) | (8) |
b(b(c(x1))) | → | b(a(b(x1))) | (9) |
a(a(b(x1))) | → | a(x1) | (10) |
a(a(c(x1))) | → | a(c(c(b(c(x1))))) | (11) |
a(b(c(x1))) | → | a(a(b(x1))) | (12) |
{c(☐), b(☐), a(☐)}
We obtain the transformed TRSc(c(a(b(x1)))) | → | c(c(x1)) | (13) |
c(c(a(c(x1)))) | → | c(c(c(c(b(c(x1)))))) | (14) |
c(c(b(c(x1)))) | → | c(c(a(b(x1)))) | (15) |
c(b(a(b(x1)))) | → | c(b(x1)) | (16) |
c(b(a(c(x1)))) | → | c(b(c(c(b(c(x1)))))) | (17) |
c(b(b(c(x1)))) | → | c(b(a(b(x1)))) | (18) |
c(a(a(b(x1)))) | → | c(a(x1)) | (19) |
c(a(a(c(x1)))) | → | c(a(c(c(b(c(x1)))))) | (20) |
c(a(b(c(x1)))) | → | c(a(a(b(x1)))) | (21) |
b(c(a(b(x1)))) | → | b(c(x1)) | (22) |
b(c(a(c(x1)))) | → | b(c(c(c(b(c(x1)))))) | (23) |
b(c(b(c(x1)))) | → | b(c(a(b(x1)))) | (24) |
b(b(a(b(x1)))) | → | b(b(x1)) | (25) |
b(b(a(c(x1)))) | → | b(b(c(c(b(c(x1)))))) | (26) |
b(b(b(c(x1)))) | → | b(b(a(b(x1)))) | (27) |
b(a(a(b(x1)))) | → | b(a(x1)) | (28) |
b(a(a(c(x1)))) | → | b(a(c(c(b(c(x1)))))) | (29) |
b(a(b(c(x1)))) | → | b(a(a(b(x1)))) | (30) |
a(c(a(b(x1)))) | → | a(c(x1)) | (31) |
a(c(a(c(x1)))) | → | a(c(c(c(b(c(x1)))))) | (32) |
a(c(b(c(x1)))) | → | a(c(a(b(x1)))) | (33) |
a(b(a(b(x1)))) | → | a(b(x1)) | (34) |
a(b(a(c(x1)))) | → | a(b(c(c(b(c(x1)))))) | (35) |
a(b(b(c(x1)))) | → | a(b(a(b(x1)))) | (36) |
a(a(a(b(x1)))) | → | a(a(x1)) | (37) |
a(a(a(c(x1)))) | → | a(a(c(c(b(c(x1)))))) | (38) |
a(a(b(c(x1)))) | → | a(a(a(b(x1)))) | (39) |
As carrier we take the set {0,...,8}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 9):
[c(x1)] | = | 3x1 + 0 |
[b(x1)] | = | 3x1 + 1 |
[a(x1)] | = | 3x1 + 2 |
There are 243 ruless (increase limit for explicit display).
[c0(x1)] | = |
x1 +
|
||||
[c3(x1)] | = |
x1 +
|
||||
[c6(x1)] | = |
x1 +
|
||||
[c1(x1)] | = |
x1 +
|
||||
[c4(x1)] | = |
x1 +
|
||||
[c7(x1)] | = |
x1 +
|
||||
[c2(x1)] | = |
x1 +
|
||||
[c5(x1)] | = |
x1 +
|
||||
[c8(x1)] | = |
x1 +
|
||||
[b0(x1)] | = |
x1 +
|
||||
[b3(x1)] | = |
x1 +
|
||||
[b6(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[b4(x1)] | = |
x1 +
|
||||
[b7(x1)] | = |
x1 +
|
||||
[b2(x1)] | = |
x1 +
|
||||
[b5(x1)] | = |
x1 +
|
||||
[b8(x1)] | = |
x1 +
|
||||
[a0(x1)] | = |
x1 +
|
||||
[a3(x1)] | = |
x1 +
|
||||
[a6(x1)] | = |
x1 +
|
||||
[a1(x1)] | = |
x1 +
|
||||
[a4(x1)] | = |
x1 +
|
||||
[a7(x1)] | = |
x1 +
|
||||
[a2(x1)] | = |
x1 +
|
||||
[a5(x1)] | = |
x1 +
|
||||
[a8(x1)] | = |
x1 +
|
a8(a5(a4(b7(x1)))) | → | a5(a7(x1)) | (43) |
a8(a5(a4(b4(x1)))) | → | a5(a4(x1)) | (44) |
b8(a5(a4(b7(x1)))) | → | b5(a7(x1)) | (70) |
b8(a5(a4(b4(x1)))) | → | b5(a4(x1)) | (71) |
b7(b5(a1(b6(x1)))) | → | b1(b6(x1)) | (82) |
b7(b5(a1(b3(x1)))) | → | b1(b3(x1)) | (83) |
b7(b5(a1(b0(x1)))) | → | b1(b0(x1)) | (84) |
c8(a5(a4(b7(x1)))) | → | c5(a7(x1)) | (97) |
c8(a5(a4(b4(x1)))) | → | c5(a4(x1)) | (98) |
c7(b5(a1(b6(x1)))) | → | c1(b6(x1)) | (109) |
c7(b5(a1(b3(x1)))) | → | c1(b3(x1)) | (110) |
c7(b5(a1(b0(x1)))) | → | c1(b0(x1)) | (111) |
b7(b2(a6(c8(x1)))) | → | b1(b0(c3(c1(b6(c8(x1)))))) | (157) |
b7(b2(a6(c5(x1)))) | → | b1(b0(c3(c1(b6(c5(x1)))))) | (158) |
b7(b2(a6(c2(x1)))) | → | b1(b0(c3(c1(b6(c2(x1)))))) | (159) |
b7(b2(a3(c7(x1)))) | → | b1(b0(c3(c1(b3(c7(x1)))))) | (160) |
b7(b2(a3(c4(x1)))) | → | b1(b0(c3(c1(b3(c4(x1)))))) | (161) |
b7(b2(a3(c1(x1)))) | → | b1(b0(c3(c1(b3(c1(x1)))))) | (162) |
b7(b2(a0(c6(x1)))) | → | b1(b0(c3(c1(b0(c6(x1)))))) | (163) |
b7(b2(a0(c3(x1)))) | → | b1(b0(c3(c1(b0(c3(x1)))))) | (164) |
b7(b2(a0(c0(x1)))) | → | b1(b0(c3(c1(b0(c0(x1)))))) | (165) |
c7(b2(a6(c8(x1)))) | → | c1(b0(c3(c1(b6(c8(x1)))))) | (184) |
c7(b2(a6(c5(x1)))) | → | c1(b0(c3(c1(b6(c5(x1)))))) | (185) |
c7(b2(a6(c2(x1)))) | → | c1(b0(c3(c1(b6(c2(x1)))))) | (186) |
c7(b2(a3(c7(x1)))) | → | c1(b0(c3(c1(b3(c7(x1)))))) | (187) |
c7(b2(a3(c4(x1)))) | → | c1(b0(c3(c1(b3(c4(x1)))))) | (188) |
c7(b2(a3(c1(x1)))) | → | c1(b0(c3(c1(b3(c1(x1)))))) | (189) |
c7(b2(a0(c6(x1)))) | → | c1(b0(c3(c1(b0(c6(x1)))))) | (190) |
c7(b2(a0(c3(x1)))) | → | c1(b0(c3(c1(b0(c3(x1)))))) | (191) |
c7(b2(a0(c0(x1)))) | → | c1(b0(c3(c1(b0(c0(x1)))))) | (192) |
There are 213 ruless (increase limit for explicit display).
[c0(x1)] | = |
|
||||||||
[c3(x1)] | = |
|
||||||||
[c6(x1)] | = |
|
||||||||
[c1(x1)] | = |
|
||||||||
[c4(x1)] | = |
|
||||||||
[c7(x1)] | = |
|
||||||||
[c2(x1)] | = |
|
||||||||
[c5(x1)] | = |
|
||||||||
[c8(x1)] | = |
|
||||||||
[b0(x1)] | = |
|
||||||||
[b3(x1)] | = |
|
||||||||
[b6(x1)] | = |
|
||||||||
[b1(x1)] | = |
|
||||||||
[b4(x1)] | = |
|
||||||||
[b7(x1)] | = |
|
||||||||
[b2(x1)] | = |
|
||||||||
[b5(x1)] | = |
|
||||||||
[b8(x1)] | = |
|
||||||||
[a0(x1)] | = |
|
||||||||
[a3(x1)] | = |
|
||||||||
[a6(x1)] | = |
|
||||||||
[a1(x1)] | = |
|
||||||||
[a4(x1)] | = |
|
||||||||
[a7(x1)] | = |
|
||||||||
[a2(x1)] | = |
|
||||||||
[a5(x1)] | = |
|
||||||||
[a8(x1)] | = |
|
There are 132 ruless (increase limit for explicit display).
[c0(x1)] | = |
x1 +
|
||||
[c3(x1)] | = |
x1 +
|
||||
[c6(x1)] | = |
x1 +
|
||||
[c1(x1)] | = |
x1 +
|
||||
[c4(x1)] | = |
x1 +
|
||||
[c7(x1)] | = |
x1 +
|
||||
[c2(x1)] | = |
x1 +
|
||||
[c5(x1)] | = |
x1 +
|
||||
[c8(x1)] | = |
x1 +
|
||||
[b0(x1)] | = |
x1 +
|
||||
[b3(x1)] | = |
x1 +
|
||||
[b6(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[b4(x1)] | = |
x1 +
|
||||
[b7(x1)] | = |
x1 +
|
||||
[b2(x1)] | = |
x1 +
|
||||
[b5(x1)] | = |
x1 +
|
||||
[b8(x1)] | = |
x1 +
|
||||
[a3(x1)] | = |
x1 +
|
||||
[a6(x1)] | = |
x1 +
|
||||
[a1(x1)] | = |
x1 +
|
||||
[a4(x1)] | = |
x1 +
|
||||
[a7(x1)] | = |
x1 +
|
||||
[a5(x1)] | = |
x1 +
|
||||
[a8(x1)] | = |
x1 +
|
c8(b6(a1(a5(x1)))) | → | b8(a7(a5(a8(x1)))) | (415) |
c5(b6(a1(a5(x1)))) | → | b5(a7(a5(a8(x1)))) | (416) |
c2(b6(a1(a5(x1)))) | → | b2(a7(a5(a8(x1)))) | (417) |
c7(b3(a1(a5(x1)))) | → | b7(a4(a5(a8(x1)))) | (418) |
c4(b3(a1(a5(x1)))) | → | b4(a4(a5(a8(x1)))) | (419) |
c1(b3(a1(a5(x1)))) | → | b1(a4(a5(a8(x1)))) | (420) |
c6(b0(a1(a5(x1)))) | → | b6(a1(a5(a8(x1)))) | (421) |
c3(b0(a1(a5(x1)))) | → | b3(a1(a5(a8(x1)))) | (422) |
c0(b0(a1(a5(x1)))) | → | b0(a1(a5(a8(x1)))) | (423) |
c8(b6(b1(a4(x1)))) | → | b8(a7(b5(a7(x1)))) | (424) |
c5(b6(b1(a4(x1)))) | → | b5(a7(b5(a7(x1)))) | (425) |
c2(b6(b1(a4(x1)))) | → | b2(a7(b5(a7(x1)))) | (426) |
c7(b3(b1(a4(x1)))) | → | b7(a4(b5(a7(x1)))) | (427) |
c4(b3(b1(a4(x1)))) | → | b4(a4(b5(a7(x1)))) | (428) |
c1(b3(b1(a4(x1)))) | → | b1(a4(b5(a7(x1)))) | (429) |
c6(b0(b1(a4(x1)))) | → | b6(a1(b5(a7(x1)))) | (430) |
c3(b0(b1(a4(x1)))) | → | b3(a1(b5(a7(x1)))) | (431) |
c0(b0(b1(a4(x1)))) | → | b0(a1(b5(a7(x1)))) | (432) |
c8(b6(c1(a3(x1)))) | → | b8(a7(c5(a6(x1)))) | (433) |
c5(b6(c1(a3(x1)))) | → | b5(a7(c5(a6(x1)))) | (434) |
c2(b6(c1(a3(x1)))) | → | b2(a7(c5(a6(x1)))) | (435) |
c7(b3(c1(a3(x1)))) | → | b7(a4(c5(a6(x1)))) | (436) |
c4(b3(c1(a3(x1)))) | → | b4(a4(c5(a6(x1)))) | (437) |
c1(b3(c1(a3(x1)))) | → | b1(a4(c5(a6(x1)))) | (438) |
c6(b0(c1(a3(x1)))) | → | b6(a1(c5(a6(x1)))) | (439) |
c3(b0(c1(a3(x1)))) | → | b3(a1(c5(a6(x1)))) | (440) |
c0(b0(c1(a3(x1)))) | → | b0(a1(c5(a6(x1)))) | (441) |
c8(b6(a1(b5(x1)))) | → | b8(a7(a5(b8(x1)))) | (442) |
c5(b6(a1(b5(x1)))) | → | b5(a7(a5(b8(x1)))) | (443) |
c2(b6(a1(b5(x1)))) | → | b2(a7(a5(b8(x1)))) | (444) |
c7(b3(a1(b5(x1)))) | → | b7(a4(a5(b8(x1)))) | (445) |
c4(b3(a1(b5(x1)))) | → | b4(a4(a5(b8(x1)))) | (446) |
c1(b3(a1(b5(x1)))) | → | b1(a4(a5(b8(x1)))) | (447) |
c6(b0(a1(b5(x1)))) | → | b6(a1(a5(b8(x1)))) | (448) |
c3(b0(a1(b5(x1)))) | → | b3(a1(a5(b8(x1)))) | (449) |
c0(b0(a1(b5(x1)))) | → | b0(a1(a5(b8(x1)))) | (450) |
c8(b6(b1(b4(x1)))) | → | b8(a7(b5(b7(x1)))) | (451) |
c5(b6(b1(b4(x1)))) | → | b5(a7(b5(b7(x1)))) | (452) |
c2(b6(b1(b4(x1)))) | → | b2(a7(b5(b7(x1)))) | (453) |
c7(b3(b1(b4(x1)))) | → | b7(a4(b5(b7(x1)))) | (454) |
c4(b3(b1(b4(x1)))) | → | b4(a4(b5(b7(x1)))) | (455) |
c1(b3(b1(b4(x1)))) | → | b1(a4(b5(b7(x1)))) | (456) |
c6(b0(b1(b4(x1)))) | → | b6(a1(b5(b7(x1)))) | (457) |
c3(b0(b1(b4(x1)))) | → | b3(a1(b5(b7(x1)))) | (458) |
c0(b0(b1(b4(x1)))) | → | b0(a1(b5(b7(x1)))) | (459) |
c8(b6(c1(b3(x1)))) | → | b8(a7(c5(b6(x1)))) | (460) |
c5(b6(c1(b3(x1)))) | → | b5(a7(c5(b6(x1)))) | (461) |
c2(b6(c1(b3(x1)))) | → | b2(a7(c5(b6(x1)))) | (462) |
c7(b3(c1(b3(x1)))) | → | b7(a4(c5(b6(x1)))) | (463) |
c4(b3(c1(b3(x1)))) | → | b4(a4(c5(b6(x1)))) | (464) |
c1(b3(c1(b3(x1)))) | → | b1(a4(c5(b6(x1)))) | (465) |
c6(b0(c1(b3(x1)))) | → | b6(a1(c5(b6(x1)))) | (466) |
c3(b0(c1(b3(x1)))) | → | b3(a1(c5(b6(x1)))) | (467) |
c0(b0(c1(b3(x1)))) | → | b0(a1(c5(b6(x1)))) | (468) |
c8(b6(a1(c5(x1)))) | → | b8(a7(a5(c8(x1)))) | (469) |
c5(b6(a1(c5(x1)))) | → | b5(a7(a5(c8(x1)))) | (470) |
c2(b6(a1(c5(x1)))) | → | b2(a7(a5(c8(x1)))) | (471) |
c7(b3(a1(c5(x1)))) | → | b7(a4(a5(c8(x1)))) | (472) |
c4(b3(a1(c5(x1)))) | → | b4(a4(a5(c8(x1)))) | (473) |
c1(b3(a1(c5(x1)))) | → | b1(a4(a5(c8(x1)))) | (474) |
c6(b0(a1(c5(x1)))) | → | b6(a1(a5(c8(x1)))) | (475) |
c3(b0(a1(c5(x1)))) | → | b3(a1(a5(c8(x1)))) | (476) |
c0(b0(a1(c5(x1)))) | → | b0(a1(a5(c8(x1)))) | (477) |
c8(b6(b1(c4(x1)))) | → | b8(a7(b5(c7(x1)))) | (478) |
c5(b6(b1(c4(x1)))) | → | b5(a7(b5(c7(x1)))) | (479) |
c2(b6(b1(c4(x1)))) | → | b2(a7(b5(c7(x1)))) | (480) |
c7(b3(b1(c4(x1)))) | → | b7(a4(b5(c7(x1)))) | (481) |
c4(b3(b1(c4(x1)))) | → | b4(a4(b5(c7(x1)))) | (482) |
c1(b3(b1(c4(x1)))) | → | b1(a4(b5(c7(x1)))) | (483) |
c6(b0(b1(c4(x1)))) | → | b6(a1(b5(c7(x1)))) | (484) |
c3(b0(b1(c4(x1)))) | → | b3(a1(b5(c7(x1)))) | (485) |
c0(b0(b1(c4(x1)))) | → | b0(a1(b5(c7(x1)))) | (486) |
c8(b6(c1(c3(x1)))) | → | b8(a7(c5(c6(x1)))) | (487) |
c5(b6(c1(c3(x1)))) | → | b5(a7(c5(c6(x1)))) | (488) |
c2(b6(c1(c3(x1)))) | → | b2(a7(c5(c6(x1)))) | (489) |
c7(b3(c1(c3(x1)))) | → | b7(a4(c5(c6(x1)))) | (490) |
c4(b3(c1(c3(x1)))) | → | b4(a4(c5(c6(x1)))) | (491) |
c1(b3(c1(c3(x1)))) | → | b1(a4(c5(c6(x1)))) | (492) |
c6(b0(c1(c3(x1)))) | → | b6(a1(c5(c6(x1)))) | (493) |
c3(b0(c1(c3(x1)))) | → | b3(a1(c5(c6(x1)))) | (494) |
c0(b0(c1(c3(x1)))) | → | b0(a1(c5(c6(x1)))) | (495) |
There are no rules.
There are no rules in the TRS. Hence, it is terminating.