The rewrite relation of the following TRS is considered.
b(a(a(b(x1)))) | → | a(b(a(b(x1)))) | (1) |
a(a(a(a(x1)))) | → | b(b(b(b(x1)))) | (2) |
b(b(a(b(x1)))) | → | b(b(a(a(x1)))) | (3) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(a(a(b(x1))))) | → | b(a(b(a(b(x1))))) | (4) |
b(a(a(a(a(x1))))) | → | b(b(b(b(b(x1))))) | (5) |
b(b(b(a(b(x1))))) | → | b(b(b(a(a(x1))))) | (6) |
a(b(a(a(b(x1))))) | → | a(a(b(a(b(x1))))) | (7) |
a(a(a(a(a(x1))))) | → | a(b(b(b(b(x1))))) | (8) |
a(b(b(a(b(x1))))) | → | a(b(b(a(a(x1))))) | (9) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(b(a(a(b(x1)))))) | → | b(b(a(b(a(b(x1)))))) | (10) |
b(b(a(a(a(a(x1)))))) | → | b(b(b(b(b(b(x1)))))) | (11) |
b(b(b(b(a(b(x1)))))) | → | b(b(b(b(a(a(x1)))))) | (12) |
b(a(b(a(a(b(x1)))))) | → | b(a(a(b(a(b(x1)))))) | (13) |
b(a(a(a(a(a(x1)))))) | → | b(a(b(b(b(b(x1)))))) | (14) |
b(a(b(b(a(b(x1)))))) | → | b(a(b(b(a(a(x1)))))) | (15) |
a(b(b(a(a(b(x1)))))) | → | a(b(a(b(a(b(x1)))))) | (16) |
a(b(a(a(a(a(x1)))))) | → | a(b(b(b(b(b(x1)))))) | (17) |
a(b(b(b(a(b(x1)))))) | → | a(b(b(b(a(a(x1)))))) | (18) |
a(a(b(a(a(b(x1)))))) | → | a(a(a(b(a(b(x1)))))) | (19) |
a(a(a(a(a(a(x1)))))) | → | a(a(b(b(b(b(x1)))))) | (20) |
a(a(b(b(a(b(x1)))))) | → | a(a(b(b(a(a(x1)))))) | (21) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(b(b(a(a(b(x1))))))) | → | b(b(b(a(b(a(b(x1))))))) | (22) |
b(b(b(a(a(a(a(x1))))))) | → | b(b(b(b(b(b(b(x1))))))) | (23) |
b(b(b(b(b(a(b(x1))))))) | → | b(b(b(b(b(a(a(x1))))))) | (24) |
b(b(a(b(a(a(b(x1))))))) | → | b(b(a(a(b(a(b(x1))))))) | (25) |
b(b(a(a(a(a(a(x1))))))) | → | b(b(a(b(b(b(b(x1))))))) | (26) |
b(b(a(b(b(a(b(x1))))))) | → | b(b(a(b(b(a(a(x1))))))) | (27) |
b(a(b(b(a(a(b(x1))))))) | → | b(a(b(a(b(a(b(x1))))))) | (28) |
b(a(b(a(a(a(a(x1))))))) | → | b(a(b(b(b(b(b(x1))))))) | (29) |
b(a(b(b(b(a(b(x1))))))) | → | b(a(b(b(b(a(a(x1))))))) | (30) |
b(a(a(b(a(a(b(x1))))))) | → | b(a(a(a(b(a(b(x1))))))) | (31) |
b(a(a(a(a(a(a(x1))))))) | → | b(a(a(b(b(b(b(x1))))))) | (32) |
b(a(a(b(b(a(b(x1))))))) | → | b(a(a(b(b(a(a(x1))))))) | (33) |
a(b(b(b(a(a(b(x1))))))) | → | a(b(b(a(b(a(b(x1))))))) | (34) |
a(b(b(a(a(a(a(x1))))))) | → | a(b(b(b(b(b(b(x1))))))) | (35) |
a(b(b(b(b(a(b(x1))))))) | → | a(b(b(b(b(a(a(x1))))))) | (36) |
a(b(a(b(a(a(b(x1))))))) | → | a(b(a(a(b(a(b(x1))))))) | (37) |
a(b(a(a(a(a(a(x1))))))) | → | a(b(a(b(b(b(b(x1))))))) | (38) |
a(b(a(b(b(a(b(x1))))))) | → | a(b(a(b(b(a(a(x1))))))) | (39) |
a(a(b(b(a(a(b(x1))))))) | → | a(a(b(a(b(a(b(x1))))))) | (40) |
a(a(b(a(a(a(a(x1))))))) | → | a(a(b(b(b(b(b(x1))))))) | (41) |
a(a(b(b(b(a(b(x1))))))) | → | a(a(b(b(b(a(a(x1))))))) | (42) |
a(a(a(b(a(a(b(x1))))))) | → | a(a(a(a(b(a(b(x1))))))) | (43) |
a(a(a(a(a(a(a(x1))))))) | → | a(a(a(b(b(b(b(x1))))))) | (44) |
a(a(a(b(b(a(b(x1))))))) | → | a(a(a(b(b(a(a(x1))))))) | (45) |
As carrier we take the set {0,...,7}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 8):
[b(x1)] | = | 2x1 + 0 |
[a(x1)] | = | 2x1 + 1 |
There are 192 ruless (increase limit for explicit display).
[b0(x1)] | = |
x1 +
|
||||
[b4(x1)] | = |
x1 +
|
||||
[b2(x1)] | = |
x1 +
|
||||
[b6(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[b5(x1)] | = |
x1 +
|
||||
[b3(x1)] | = |
x1 +
|
||||
[b7(x1)] | = |
x1 +
|
||||
[a0(x1)] | = |
x1 +
|
||||
[a4(x1)] | = |
x1 +
|
||||
[a2(x1)] | = |
x1 +
|
||||
[a6(x1)] | = |
x1 +
|
||||
[a1(x1)] | = |
x1 +
|
||||
[a5(x1)] | = |
x1 +
|
||||
[a3(x1)] | = |
x1 +
|
||||
[a7(x1)] | = |
x1 +
|
There are 119 ruless (increase limit for explicit display).
b0(a0(a1(b3(b6(b4(b0(x1))))))) | → | b0(a0(b1(a2(b5(b2(b4(x1))))))) | (238) |
b4(a0(a1(b3(b6(b4(b0(x1))))))) | → | b4(a0(b1(a2(b5(b2(b4(x1))))))) | (239) |
b2(a4(a1(b3(b6(b4(b0(x1))))))) | → | b2(a4(b1(a2(b5(b2(b4(x1))))))) | (240) |
b6(a4(a1(b3(b6(b4(b0(x1))))))) | → | b6(a4(b1(a2(b5(b2(b4(x1))))))) | (241) |
b1(a2(a5(b3(b6(b4(b0(x1))))))) | → | b1(a2(b5(a2(b5(b2(b4(x1))))))) | (242) |
b5(a2(a5(b3(b6(b4(b0(x1))))))) | → | b5(a2(b5(a2(b5(b2(b4(x1))))))) | (243) |
b3(a6(a5(b3(b6(b4(b0(x1))))))) | → | b3(a6(b5(a2(b5(b2(b4(x1))))))) | (244) |
b7(a6(a5(b3(b6(b4(b0(x1))))))) | → | b7(a6(b5(a2(b5(b2(b4(x1))))))) | (245) |
b0(a0(a1(b3(b6(b4(a0(x1))))))) | → | b0(a0(b1(a2(b5(b2(a4(x1))))))) | (246) |
b4(a0(a1(b3(b6(b4(a0(x1))))))) | → | b4(a0(b1(a2(b5(b2(a4(x1))))))) | (247) |
b2(a4(a1(b3(b6(b4(a0(x1))))))) | → | b2(a4(b1(a2(b5(b2(a4(x1))))))) | (248) |
b6(a4(a1(b3(b6(b4(a0(x1))))))) | → | b6(a4(b1(a2(b5(b2(a4(x1))))))) | (249) |
b1(a2(a5(b3(b6(b4(a0(x1))))))) | → | b1(a2(b5(a2(b5(b2(a4(x1))))))) | (250) |
b5(a2(a5(b3(b6(b4(a0(x1))))))) | → | b5(a2(b5(a2(b5(b2(a4(x1))))))) | (251) |
b3(a6(a5(b3(b6(b4(a0(x1))))))) | → | b3(a6(b5(a2(b5(b2(a4(x1))))))) | (252) |
b7(a6(a5(b3(b6(b4(a0(x1))))))) | → | b7(a6(b5(a2(b5(b2(a4(x1))))))) | (253) |
b0(a0(a1(b3(a6(b5(a2(x1))))))) | → | b0(a0(b1(a2(a5(b3(a6(x1))))))) | (254) |
b4(a0(a1(b3(a6(b5(a2(x1))))))) | → | b4(a0(b1(a2(a5(b3(a6(x1))))))) | (255) |
b2(a4(a1(b3(a6(b5(a2(x1))))))) | → | b2(a4(b1(a2(a5(b3(a6(x1))))))) | (256) |
b6(a4(a1(b3(a6(b5(a2(x1))))))) | → | b6(a4(b1(a2(a5(b3(a6(x1))))))) | (257) |
b1(a2(a5(b3(a6(b5(a2(x1))))))) | → | b1(a2(b5(a2(a5(b3(a6(x1))))))) | (258) |
b5(a2(a5(b3(a6(b5(a2(x1))))))) | → | b5(a2(b5(a2(a5(b3(a6(x1))))))) | (259) |
b3(a6(a5(b3(a6(b5(a2(x1))))))) | → | b3(a6(b5(a2(a5(b3(a6(x1))))))) | (260) |
b7(a6(a5(b3(a6(b5(a2(x1))))))) | → | b7(a6(b5(a2(a5(b3(a6(x1))))))) | (261) |
a2(a5(a3(a7(a7(b7(b6(x1))))))) | → | b2(b4(b0(b0(a0(b1(b2(x1))))))) | (262) |
b0(a0(b1(b2(b4(b0(b0(x1))))))) | → | a0(a1(b3(b6(b4(b0(b0(x1))))))) | (263) |
b4(a0(b1(b2(b4(b0(b0(x1))))))) | → | a4(a1(b3(b6(b4(b0(b0(x1))))))) | (264) |
b6(a4(b1(b2(b4(b0(b0(x1))))))) | → | a6(a5(b3(b6(b4(b0(b0(x1))))))) | (265) |
b1(a2(b5(b2(b4(b0(b0(x1))))))) | → | a1(a3(b7(b6(b4(b0(b0(x1))))))) | (266) |
b5(a2(b5(b2(b4(b0(b0(x1))))))) | → | a5(a3(b7(b6(b4(b0(b0(x1))))))) | (267) |
b7(a6(b5(b2(b4(b0(b0(x1))))))) | → | a7(a7(b7(b6(b4(b0(b0(x1))))))) | (268) |
b0(a0(b1(b2(a4(b1(b2(x1))))))) | → | a0(a1(b3(b6(a4(b1(b2(x1))))))) | (269) |
b4(a0(b1(b2(a4(b1(b2(x1))))))) | → | a4(a1(b3(b6(a4(b1(b2(x1))))))) | (270) |
b6(a4(b1(b2(a4(b1(b2(x1))))))) | → | a6(a5(b3(b6(a4(b1(b2(x1))))))) | (271) |
b1(a2(b5(b2(a4(b1(b2(x1))))))) | → | a1(a3(b7(b6(a4(b1(b2(x1))))))) | (272) |
b5(a2(b5(b2(a4(b1(b2(x1))))))) | → | a5(a3(b7(b6(a4(b1(b2(x1))))))) | (273) |
b7(a6(b5(b2(a4(b1(b2(x1))))))) | → | a7(a7(b7(b6(a4(b1(b2(x1))))))) | (274) |
b0(a0(b1(b2(b4(a0(b1(x1))))))) | → | a0(a1(b3(b6(b4(a0(b1(x1))))))) | (275) |
b4(a0(b1(b2(b4(a0(b1(x1))))))) | → | a4(a1(b3(b6(b4(a0(b1(x1))))))) | (276) |
b6(a4(b1(b2(b4(a0(b1(x1))))))) | → | a6(a5(b3(b6(b4(a0(b1(x1))))))) | (277) |
b1(a2(b5(b2(b4(a0(b1(x1))))))) | → | a1(a3(b7(b6(b4(a0(b1(x1))))))) | (278) |
b5(a2(b5(b2(b4(a0(b1(x1))))))) | → | a5(a3(b7(b6(b4(a0(b1(x1))))))) | (279) |
b7(a6(b5(b2(b4(a0(b1(x1))))))) | → | a7(a7(b7(b6(b4(a0(b1(x1))))))) | (280) |
b0(a0(b1(b2(a4(a1(b3(x1))))))) | → | a0(a1(b3(b6(a4(a1(b3(x1))))))) | (281) |
b4(a0(b1(b2(a4(a1(b3(x1))))))) | → | a4(a1(b3(b6(a4(a1(b3(x1))))))) | (282) |
b6(a4(b1(b2(a4(a1(b3(x1))))))) | → | a6(a5(b3(b6(a4(a1(b3(x1))))))) | (283) |
b1(a2(b5(b2(a4(a1(b3(x1))))))) | → | a1(a3(b7(b6(a4(a1(b3(x1))))))) | (284) |
b5(a2(b5(b2(a4(a1(b3(x1))))))) | → | a5(a3(b7(b6(a4(a1(b3(x1))))))) | (285) |
b7(a6(b5(b2(a4(a1(b3(x1))))))) | → | a7(a7(b7(b6(a4(a1(b3(x1))))))) | (286) |
b0(a0(b1(b2(b4(b0(a0(x1))))))) | → | a0(a1(b3(b6(b4(b0(a0(x1))))))) | (287) |
b4(a0(b1(b2(b4(b0(a0(x1))))))) | → | a4(a1(b3(b6(b4(b0(a0(x1))))))) | (288) |
b6(a4(b1(b2(b4(b0(a0(x1))))))) | → | a6(a5(b3(b6(b4(b0(a0(x1))))))) | (289) |
b1(a2(b5(b2(b4(b0(a0(x1))))))) | → | a1(a3(b7(b6(b4(b0(a0(x1))))))) | (290) |
b5(a2(b5(b2(b4(b0(a0(x1))))))) | → | a5(a3(b7(b6(b4(b0(a0(x1))))))) | (291) |
b7(a6(b5(b2(b4(b0(a0(x1))))))) | → | a7(a7(b7(b6(b4(b0(a0(x1))))))) | (292) |
b0(a0(b1(b2(a4(b1(a2(x1))))))) | → | a0(a1(b3(b6(a4(b1(a2(x1))))))) | (293) |
b4(a0(b1(b2(a4(b1(a2(x1))))))) | → | a4(a1(b3(b6(a4(b1(a2(x1))))))) | (294) |
b6(a4(b1(b2(a4(b1(a2(x1))))))) | → | a6(a5(b3(b6(a4(b1(a2(x1))))))) | (295) |
b1(a2(b5(b2(a4(b1(a2(x1))))))) | → | a1(a3(b7(b6(a4(b1(a2(x1))))))) | (296) |
b5(a2(b5(b2(a4(b1(a2(x1))))))) | → | a5(a3(b7(b6(a4(b1(a2(x1))))))) | (297) |
b7(a6(b5(b2(a4(b1(a2(x1))))))) | → | a7(a7(b7(b6(a4(b1(a2(x1))))))) | (298) |
b0(a0(b1(b2(b4(a0(a1(x1))))))) | → | a0(a1(b3(b6(b4(a0(a1(x1))))))) | (299) |
b4(a0(b1(b2(b4(a0(a1(x1))))))) | → | a4(a1(b3(b6(b4(a0(a1(x1))))))) | (300) |
b6(a4(b1(b2(b4(a0(a1(x1))))))) | → | a6(a5(b3(b6(b4(a0(a1(x1))))))) | (301) |
b1(a2(b5(b2(b4(a0(a1(x1))))))) | → | a1(a3(b7(b6(b4(a0(a1(x1))))))) | (302) |
b5(a2(b5(b2(b4(a0(a1(x1))))))) | → | a5(a3(b7(b6(b4(a0(a1(x1))))))) | (303) |
b7(a6(b5(b2(b4(a0(a1(x1))))))) | → | a7(a7(b7(b6(b4(a0(a1(x1))))))) | (304) |
b0(a0(b1(b2(a4(a1(a3(x1))))))) | → | a0(a1(b3(b6(a4(a1(a3(x1))))))) | (305) |
b4(a0(b1(b2(a4(a1(a3(x1))))))) | → | a4(a1(b3(b6(a4(a1(a3(x1))))))) | (306) |
b6(a4(b1(b2(a4(a1(a3(x1))))))) | → | a6(a5(b3(b6(a4(a1(a3(x1))))))) | (307) |
b1(a2(b5(b2(a4(a1(a3(x1))))))) | → | a1(a3(b7(b6(a4(a1(a3(x1))))))) | (308) |
b5(a2(b5(b2(a4(a1(a3(x1))))))) | → | a5(a3(b7(b6(a4(a1(a3(x1))))))) | (309) |
b7(a6(b5(b2(a4(a1(a3(x1))))))) | → | a7(a7(b7(b6(a4(a1(a3(x1))))))) | (310) |
[b0(x1)] | = |
|
||||||||
[b4(x1)] | = |
|
||||||||
[b2(x1)] | = |
|
||||||||
[b6(x1)] | = |
|
||||||||
[b1(x1)] | = |
|
||||||||
[b5(x1)] | = |
|
||||||||
[b3(x1)] | = |
|
||||||||
[b7(x1)] | = |
|
||||||||
[a0(x1)] | = |
|
||||||||
[a4(x1)] | = |
|
||||||||
[a2(x1)] | = |
|
||||||||
[a6(x1)] | = |
|
||||||||
[a1(x1)] | = |
|
||||||||
[a5(x1)] | = |
|
||||||||
[a3(x1)] | = |
|
||||||||
[a7(x1)] | = |
|
b0(a0(a1(b3(b6(b4(b0(x1))))))) | → | b0(a0(b1(a2(b5(b2(b4(x1))))))) | (238) |
b4(a0(a1(b3(b6(b4(b0(x1))))))) | → | b4(a0(b1(a2(b5(b2(b4(x1))))))) | (239) |
b2(a4(a1(b3(b6(b4(b0(x1))))))) | → | b2(a4(b1(a2(b5(b2(b4(x1))))))) | (240) |
b6(a4(a1(b3(b6(b4(b0(x1))))))) | → | b6(a4(b1(a2(b5(b2(b4(x1))))))) | (241) |
b1(a2(a5(b3(b6(b4(b0(x1))))))) | → | b1(a2(b5(a2(b5(b2(b4(x1))))))) | (242) |
b5(a2(a5(b3(b6(b4(b0(x1))))))) | → | b5(a2(b5(a2(b5(b2(b4(x1))))))) | (243) |
b3(a6(a5(b3(b6(b4(b0(x1))))))) | → | b3(a6(b5(a2(b5(b2(b4(x1))))))) | (244) |
b7(a6(a5(b3(b6(b4(b0(x1))))))) | → | b7(a6(b5(a2(b5(b2(b4(x1))))))) | (245) |
b0(a0(a1(b3(b6(b4(a0(x1))))))) | → | b0(a0(b1(a2(b5(b2(a4(x1))))))) | (246) |
b4(a0(a1(b3(b6(b4(a0(x1))))))) | → | b4(a0(b1(a2(b5(b2(a4(x1))))))) | (247) |
b2(a4(a1(b3(b6(b4(a0(x1))))))) | → | b2(a4(b1(a2(b5(b2(a4(x1))))))) | (248) |
b6(a4(a1(b3(b6(b4(a0(x1))))))) | → | b6(a4(b1(a2(b5(b2(a4(x1))))))) | (249) |
b1(a2(a5(b3(b6(b4(a0(x1))))))) | → | b1(a2(b5(a2(b5(b2(a4(x1))))))) | (250) |
b5(a2(a5(b3(b6(b4(a0(x1))))))) | → | b5(a2(b5(a2(b5(b2(a4(x1))))))) | (251) |
b3(a6(a5(b3(b6(b4(a0(x1))))))) | → | b3(a6(b5(a2(b5(b2(a4(x1))))))) | (252) |
b7(a6(a5(b3(b6(b4(a0(x1))))))) | → | b7(a6(b5(a2(b5(b2(a4(x1))))))) | (253) |
b0(a0(a1(b3(a6(b5(a2(x1))))))) | → | b0(a0(b1(a2(a5(b3(a6(x1))))))) | (254) |
b4(a0(a1(b3(a6(b5(a2(x1))))))) | → | b4(a0(b1(a2(a5(b3(a6(x1))))))) | (255) |
b2(a4(a1(b3(a6(b5(a2(x1))))))) | → | b2(a4(b1(a2(a5(b3(a6(x1))))))) | (256) |
b6(a4(a1(b3(a6(b5(a2(x1))))))) | → | b6(a4(b1(a2(a5(b3(a6(x1))))))) | (257) |
b1(a2(a5(b3(a6(b5(a2(x1))))))) | → | b1(a2(b5(a2(a5(b3(a6(x1))))))) | (258) |
b5(a2(a5(b3(a6(b5(a2(x1))))))) | → | b5(a2(b5(a2(a5(b3(a6(x1))))))) | (259) |
b3(a6(a5(b3(a6(b5(a2(x1))))))) | → | b3(a6(b5(a2(a5(b3(a6(x1))))))) | (260) |
b7(a6(a5(b3(a6(b5(a2(x1))))))) | → | b7(a6(b5(a2(a5(b3(a6(x1))))))) | (261) |
b0(a0(b1(b2(b4(b0(b0(x1))))))) | → | a0(a1(b3(b6(b4(b0(b0(x1))))))) | (263) |
b4(a0(b1(b2(b4(b0(b0(x1))))))) | → | a4(a1(b3(b6(b4(b0(b0(x1))))))) | (264) |
b6(a4(b1(b2(b4(b0(b0(x1))))))) | → | a6(a5(b3(b6(b4(b0(b0(x1))))))) | (265) |
b1(a2(b5(b2(b4(b0(b0(x1))))))) | → | a1(a3(b7(b6(b4(b0(b0(x1))))))) | (266) |
b5(a2(b5(b2(b4(b0(b0(x1))))))) | → | a5(a3(b7(b6(b4(b0(b0(x1))))))) | (267) |
b7(a6(b5(b2(b4(b0(b0(x1))))))) | → | a7(a7(b7(b6(b4(b0(b0(x1))))))) | (268) |
b0(a0(b1(b2(a4(b1(b2(x1))))))) | → | a0(a1(b3(b6(a4(b1(b2(x1))))))) | (269) |
b4(a0(b1(b2(a4(b1(b2(x1))))))) | → | a4(a1(b3(b6(a4(b1(b2(x1))))))) | (270) |
b6(a4(b1(b2(a4(b1(b2(x1))))))) | → | a6(a5(b3(b6(a4(b1(b2(x1))))))) | (271) |
b1(a2(b5(b2(a4(b1(b2(x1))))))) | → | a1(a3(b7(b6(a4(b1(b2(x1))))))) | (272) |
b5(a2(b5(b2(a4(b1(b2(x1))))))) | → | a5(a3(b7(b6(a4(b1(b2(x1))))))) | (273) |
b7(a6(b5(b2(a4(b1(b2(x1))))))) | → | a7(a7(b7(b6(a4(b1(b2(x1))))))) | (274) |
b0(a0(b1(b2(b4(a0(b1(x1))))))) | → | a0(a1(b3(b6(b4(a0(b1(x1))))))) | (275) |
b4(a0(b1(b2(b4(a0(b1(x1))))))) | → | a4(a1(b3(b6(b4(a0(b1(x1))))))) | (276) |
b6(a4(b1(b2(b4(a0(b1(x1))))))) | → | a6(a5(b3(b6(b4(a0(b1(x1))))))) | (277) |
b1(a2(b5(b2(b4(a0(b1(x1))))))) | → | a1(a3(b7(b6(b4(a0(b1(x1))))))) | (278) |
b5(a2(b5(b2(b4(a0(b1(x1))))))) | → | a5(a3(b7(b6(b4(a0(b1(x1))))))) | (279) |
b7(a6(b5(b2(b4(a0(b1(x1))))))) | → | a7(a7(b7(b6(b4(a0(b1(x1))))))) | (280) |
b0(a0(b1(b2(a4(a1(b3(x1))))))) | → | a0(a1(b3(b6(a4(a1(b3(x1))))))) | (281) |
b4(a0(b1(b2(a4(a1(b3(x1))))))) | → | a4(a1(b3(b6(a4(a1(b3(x1))))))) | (282) |
b6(a4(b1(b2(a4(a1(b3(x1))))))) | → | a6(a5(b3(b6(a4(a1(b3(x1))))))) | (283) |
b1(a2(b5(b2(a4(a1(b3(x1))))))) | → | a1(a3(b7(b6(a4(a1(b3(x1))))))) | (284) |
b5(a2(b5(b2(a4(a1(b3(x1))))))) | → | a5(a3(b7(b6(a4(a1(b3(x1))))))) | (285) |
b7(a6(b5(b2(a4(a1(b3(x1))))))) | → | a7(a7(b7(b6(a4(a1(b3(x1))))))) | (286) |
b0(a0(b1(b2(b4(b0(a0(x1))))))) | → | a0(a1(b3(b6(b4(b0(a0(x1))))))) | (287) |
b4(a0(b1(b2(b4(b0(a0(x1))))))) | → | a4(a1(b3(b6(b4(b0(a0(x1))))))) | (288) |
b6(a4(b1(b2(b4(b0(a0(x1))))))) | → | a6(a5(b3(b6(b4(b0(a0(x1))))))) | (289) |
b1(a2(b5(b2(b4(b0(a0(x1))))))) | → | a1(a3(b7(b6(b4(b0(a0(x1))))))) | (290) |
b5(a2(b5(b2(b4(b0(a0(x1))))))) | → | a5(a3(b7(b6(b4(b0(a0(x1))))))) | (291) |
b7(a6(b5(b2(b4(b0(a0(x1))))))) | → | a7(a7(b7(b6(b4(b0(a0(x1))))))) | (292) |
b0(a0(b1(b2(a4(b1(a2(x1))))))) | → | a0(a1(b3(b6(a4(b1(a2(x1))))))) | (293) |
b4(a0(b1(b2(a4(b1(a2(x1))))))) | → | a4(a1(b3(b6(a4(b1(a2(x1))))))) | (294) |
b6(a4(b1(b2(a4(b1(a2(x1))))))) | → | a6(a5(b3(b6(a4(b1(a2(x1))))))) | (295) |
b1(a2(b5(b2(a4(b1(a2(x1))))))) | → | a1(a3(b7(b6(a4(b1(a2(x1))))))) | (296) |
b5(a2(b5(b2(a4(b1(a2(x1))))))) | → | a5(a3(b7(b6(a4(b1(a2(x1))))))) | (297) |
b7(a6(b5(b2(a4(b1(a2(x1))))))) | → | a7(a7(b7(b6(a4(b1(a2(x1))))))) | (298) |
b0(a0(b1(b2(b4(a0(a1(x1))))))) | → | a0(a1(b3(b6(b4(a0(a1(x1))))))) | (299) |
b4(a0(b1(b2(b4(a0(a1(x1))))))) | → | a4(a1(b3(b6(b4(a0(a1(x1))))))) | (300) |
b6(a4(b1(b2(b4(a0(a1(x1))))))) | → | a6(a5(b3(b6(b4(a0(a1(x1))))))) | (301) |
b1(a2(b5(b2(b4(a0(a1(x1))))))) | → | a1(a3(b7(b6(b4(a0(a1(x1))))))) | (302) |
b5(a2(b5(b2(b4(a0(a1(x1))))))) | → | a5(a3(b7(b6(b4(a0(a1(x1))))))) | (303) |
b7(a6(b5(b2(b4(a0(a1(x1))))))) | → | a7(a7(b7(b6(b4(a0(a1(x1))))))) | (304) |
b0(a0(b1(b2(a4(a1(a3(x1))))))) | → | a0(a1(b3(b6(a4(a1(a3(x1))))))) | (305) |
b4(a0(b1(b2(a4(a1(a3(x1))))))) | → | a4(a1(b3(b6(a4(a1(a3(x1))))))) | (306) |
b6(a4(b1(b2(a4(a1(a3(x1))))))) | → | a6(a5(b3(b6(a4(a1(a3(x1))))))) | (307) |
b1(a2(b5(b2(a4(a1(a3(x1))))))) | → | a1(a3(b7(b6(a4(a1(a3(x1))))))) | (308) |
b5(a2(b5(b2(a4(a1(a3(x1))))))) | → | a5(a3(b7(b6(a4(a1(a3(x1))))))) | (309) |
b7(a6(b5(b2(a4(a1(a3(x1))))))) | → | a7(a7(b7(b6(a4(a1(a3(x1))))))) | (310) |
[b0(x1)] | = |
x1 +
|
||||
[b4(x1)] | = |
x1 +
|
||||
[b2(x1)] | = |
x1 +
|
||||
[b6(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[b7(x1)] | = |
x1 +
|
||||
[a0(x1)] | = |
x1 +
|
||||
[a2(x1)] | = |
x1 +
|
||||
[a5(x1)] | = |
x1 +
|
||||
[a3(x1)] | = |
x1 +
|
||||
[a7(x1)] | = |
x1 +
|
a2(a5(a3(a7(a7(b7(b6(x1))))))) | → | b2(b4(b0(b0(a0(b1(b2(x1))))))) | (262) |
There are no rules.
There are no rules in the TRS. Hence, it is terminating.