The rewrite relation of the following TRS is considered.
a(a(x1)) | → | x1 | (1) |
a(b(b(a(x1)))) | → | a(a(b(a(b(b(x1)))))) | (2) |
We split R in the relative problem D/R-D and R-D, where the rules D
a(a(x1)) | → | x1 | (1) |
{b(☐), a(☐)}
We obtain the transformed TRSb(a(a(x1))) | → | b(x1) | (3) |
a(a(a(x1))) | → | a(x1) | (4) |
b(a(b(b(a(x1))))) | → | b(a(a(b(a(b(b(x1))))))) | (5) |
a(a(b(b(a(x1))))) | → | a(a(a(b(a(b(b(x1))))))) | (6) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(a(a(x1)))) | → | b(b(x1)) | (7) |
b(a(a(a(x1)))) | → | b(a(x1)) | (8) |
a(b(a(a(x1)))) | → | a(b(x1)) | (9) |
a(a(a(a(x1)))) | → | a(a(x1)) | (10) |
b(b(a(b(b(a(x1)))))) | → | b(b(a(a(b(a(b(b(x1)))))))) | (11) |
b(a(a(b(b(a(x1)))))) | → | b(a(a(a(b(a(b(b(x1)))))))) | (12) |
a(b(a(b(b(a(x1)))))) | → | a(b(a(a(b(a(b(b(x1)))))))) | (13) |
a(a(a(b(b(a(x1)))))) | → | a(a(a(a(b(a(b(b(x1)))))))) | (14) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(b(a(a(x1))))) | → | b(b(b(x1))) | (15) |
b(b(a(a(a(x1))))) | → | b(b(a(x1))) | (16) |
b(a(b(a(a(x1))))) | → | b(a(b(x1))) | (17) |
b(a(a(a(a(x1))))) | → | b(a(a(x1))) | (18) |
a(b(b(a(a(x1))))) | → | a(b(b(x1))) | (19) |
a(b(a(a(a(x1))))) | → | a(b(a(x1))) | (20) |
a(a(b(a(a(x1))))) | → | a(a(b(x1))) | (21) |
a(a(a(a(a(x1))))) | → | a(a(a(x1))) | (22) |
b(b(b(a(b(b(a(x1))))))) | → | b(b(b(a(a(b(a(b(b(x1))))))))) | (23) |
b(b(a(a(b(b(a(x1))))))) | → | b(b(a(a(a(b(a(b(b(x1))))))))) | (24) |
b(a(b(a(b(b(a(x1))))))) | → | b(a(b(a(a(b(a(b(b(x1))))))))) | (25) |
b(a(a(a(b(b(a(x1))))))) | → | b(a(a(a(a(b(a(b(b(x1))))))))) | (26) |
a(b(b(a(b(b(a(x1))))))) | → | a(b(b(a(a(b(a(b(b(x1))))))))) | (27) |
a(b(a(a(b(b(a(x1))))))) | → | a(b(a(a(a(b(a(b(b(x1))))))))) | (28) |
a(a(b(a(b(b(a(x1))))))) | → | a(a(b(a(a(b(a(b(b(x1))))))))) | (29) |
a(a(a(a(b(b(a(x1))))))) | → | a(a(a(a(a(b(a(b(b(x1))))))))) | (30) |
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 128 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 +
|
a7(a7(a7(a7(a7(x1))))) | → | a7(a7(a7(x1))) | (31) |
a7(a7(a7(a7(a3(x1))))) | → | a7(a7(a3(x1))) | (32) |
a7(a7(a7(a3(a5(x1))))) | → | a7(a3(a5(x1))) | (33) |
a7(a7(a7(a3(a1(x1))))) | → | a7(a3(a1(x1))) | (34) |
a7(a7(a3(a5(a6(x1))))) | → | a3(a5(a6(x1))) | (35) |
a7(a7(a3(a5(a2(x1))))) | → | a3(a5(a2(x1))) | (36) |
a7(a7(a3(a1(a4(x1))))) | → | a3(a1(a4(x1))) | (37) |
a7(a7(a3(a1(a0(x1))))) | → | a3(a1(a0(x1))) | (38) |
a5(a6(b7(a7(a7(x1))))) | → | a5(a6(b7(x1))) | (39) |
a5(a6(b7(a7(a3(x1))))) | → | a5(a6(b3(x1))) | (40) |
a5(a6(b7(a3(a5(x1))))) | → | a5(a2(b5(x1))) | (41) |
a5(a6(b7(a3(a1(x1))))) | → | a5(a2(b1(x1))) | (42) |
a5(a6(b3(a1(a4(x1))))) | → | a1(a0(b4(x1))) | (45) |
a5(a6(b3(a1(a0(x1))))) | → | a1(a0(b0(x1))) | (46) |
a6(b7(a7(a7(a7(x1))))) | → | a6(b7(a7(x1))) | (47) |
a6(b7(a7(a7(a3(x1))))) | → | a6(b7(a3(x1))) | (48) |
a6(b7(a7(a3(a5(x1))))) | → | a6(b3(a5(x1))) | (49) |
a6(b7(a7(a3(a1(x1))))) | → | a6(b3(a1(x1))) | (50) |
a6(b7(a3(a5(a6(x1))))) | → | a2(b5(a6(x1))) | (51) |
a6(b7(a3(a5(a2(x1))))) | → | a2(b5(a2(x1))) | (52) |
a6(b7(a3(a1(a4(x1))))) | → | a2(b1(a4(x1))) | (53) |
a6(b7(a3(a1(a0(x1))))) | → | a2(b1(a0(x1))) | (54) |
a4(b6(b7(a7(a7(x1))))) | → | a4(b6(b7(x1))) | (55) |
a4(b6(b7(a7(a3(x1))))) | → | a4(b6(b3(x1))) | (56) |
a4(b6(b7(a3(a5(x1))))) | → | a4(b2(b5(x1))) | (57) |
a4(b6(b7(a3(a1(x1))))) | → | a4(b2(b1(x1))) | (58) |
a4(b6(b3(a5(a6(x1))))) | → | a0(b4(b6(x1))) | (59) |
a4(b6(b3(a5(a2(x1))))) | → | a0(b4(b2(x1))) | (60) |
a4(b6(b3(a1(a4(x1))))) | → | a0(b0(b4(x1))) | (61) |
a4(b6(b3(a1(a0(x1))))) | → | a0(b0(b0(x1))) | (62) |
b7(a7(a7(a7(a7(x1))))) | → | b7(a7(a7(x1))) | (63) |
b7(a7(a7(a7(a3(x1))))) | → | b7(a7(a3(x1))) | (64) |
b7(a7(a7(a3(a5(x1))))) | → | b7(a3(a5(x1))) | (65) |
b7(a7(a7(a3(a1(x1))))) | → | b7(a3(a1(x1))) | (66) |
b7(a7(a3(a5(a6(x1))))) | → | b3(a5(a6(x1))) | (67) |
b7(a7(a3(a5(a2(x1))))) | → | b3(a5(a2(x1))) | (68) |
b7(a7(a3(a1(a4(x1))))) | → | b3(a1(a4(x1))) | (69) |
b7(a7(a3(a1(a0(x1))))) | → | b3(a1(a0(x1))) | (70) |
b5(a6(b7(a7(a7(x1))))) | → | b5(a6(b7(x1))) | (71) |
b5(a6(b7(a7(a3(x1))))) | → | b5(a6(b3(x1))) | (72) |
b5(a6(b7(a3(a5(x1))))) | → | b5(a2(b5(x1))) | (73) |
b5(a6(b7(a3(a1(x1))))) | → | b5(a2(b1(x1))) | (74) |
b5(a6(b3(a1(a4(x1))))) | → | b1(a0(b4(x1))) | (77) |
b5(a6(b3(a1(a0(x1))))) | → | b1(a0(b0(x1))) | (78) |
b6(b7(a7(a7(a7(x1))))) | → | b6(b7(a7(x1))) | (79) |
b6(b7(a7(a7(a3(x1))))) | → | b6(b7(a3(x1))) | (80) |
b6(b7(a7(a3(a5(x1))))) | → | b6(b3(a5(x1))) | (81) |
b6(b7(a7(a3(a1(x1))))) | → | b6(b3(a1(x1))) | (82) |
b6(b7(a3(a5(a6(x1))))) | → | b2(b5(a6(x1))) | (83) |
b6(b7(a3(a5(a2(x1))))) | → | b2(b5(a2(x1))) | (84) |
b6(b7(a3(a1(a4(x1))))) | → | b2(b1(a4(x1))) | (85) |
b6(b7(a3(a1(a0(x1))))) | → | b2(b1(a0(x1))) | (86) |
b4(b6(b7(a7(a7(x1))))) | → | b4(b6(b7(x1))) | (87) |
b4(b6(b7(a7(a3(x1))))) | → | b4(b6(b3(x1))) | (88) |
b4(b6(b7(a3(a5(x1))))) | → | b4(b2(b5(x1))) | (89) |
b4(b6(b7(a3(a1(x1))))) | → | b4(b2(b1(x1))) | (90) |
b4(b6(b3(a5(a6(x1))))) | → | b0(b4(b6(x1))) | (91) |
b4(b6(b3(a5(a2(x1))))) | → | b0(b4(b2(x1))) | (92) |
b4(b6(b3(a1(a4(x1))))) | → | b0(b0(b4(x1))) | (93) |
b4(b6(b3(a1(a0(x1))))) | → | b0(b0(b0(x1))) | (94) |
a7(a3(a1(a4(b2(b1(a4(x1))))))) | → | a7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (101) |
a5(a2(b1(a4(b2(b1(a4(x1))))))) | → | a5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (109) |
a6(b3(a1(a4(b2(b1(a4(x1))))))) | → | a6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (117) |
a4(b2(b1(a4(b2(b1(a4(x1))))))) | → | a4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (125) |
b7(a3(a1(a4(b2(b1(a4(x1))))))) | → | b7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (133) |
b5(a2(b1(a4(b2(b1(a4(x1))))))) | → | b5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (141) |
b6(b3(a1(a4(b2(b1(a4(x1))))))) | → | b6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (149) |
b4(b2(b1(a4(b2(b1(a4(x1))))))) | → | b4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (157) |
a6(a5(b3(a6(a5(x1))))) | → | b6(a4(a1(x1))) | (159) |
a2(a5(b3(a6(a5(x1))))) | → | b2(a4(a1(x1))) | (160) |
a6(a5(b3(a6(b5(x1))))) | → | b6(a4(b1(x1))) | (161) |
a2(a5(b3(a6(b5(x1))))) | → | b2(a4(b1(x1))) | (162) |
a7(b7(b6(a4(a1(a3(a7(x1))))))) | → | b7(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) | (163) |
a3(b7(b6(a4(a1(a3(a7(x1))))))) | → | b3(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) | (164) |
a5(b3(b6(a4(a1(a3(a7(x1))))))) | → | b5(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) | (165) |
a1(b3(b6(a4(a1(a3(a7(x1))))))) | → | b1(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) | (166) |
a6(b5(b2(a4(a1(a3(a7(x1))))))) | → | b6(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) | (167) |
a2(b5(b2(a4(a1(a3(a7(x1))))))) | → | b2(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) | (168) |
a0(b1(b2(a4(a1(a3(a7(x1))))))) | → | b0(b0(a0(b1(a2(a5(a3(a7(a7(x1))))))))) | (169) |
a7(b7(b6(a4(b1(a2(a5(x1))))))) | → | b7(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) | (170) |
a3(b7(b6(a4(b1(a2(a5(x1))))))) | → | b3(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) | (171) |
a5(b3(b6(a4(b1(a2(a5(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) | (172) |
a1(b3(b6(a4(b1(a2(a5(x1))))))) | → | b1(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) | (173) |
a6(b5(b2(a4(b1(a2(a5(x1))))))) | → | b6(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) | (174) |
a2(b5(b2(a4(b1(a2(a5(x1))))))) | → | b2(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) | (175) |
a0(b1(b2(a4(b1(a2(a5(x1))))))) | → | b0(b0(a0(b1(a2(a5(b3(a6(a5(x1))))))))) | (176) |
a7(b7(b6(a4(a1(b3(a6(x1))))))) | → | b7(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) | (177) |
a3(b7(b6(a4(a1(b3(a6(x1))))))) | → | b3(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) | (178) |
a5(b3(b6(a4(a1(b3(a6(x1))))))) | → | b5(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) | (179) |
a1(b3(b6(a4(a1(b3(a6(x1))))))) | → | b1(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) | (180) |
a6(b5(b2(a4(a1(b3(a6(x1))))))) | → | b6(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) | (181) |
a2(b5(b2(a4(a1(b3(a6(x1))))))) | → | b2(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) | (182) |
a0(b1(b2(a4(a1(b3(a6(x1))))))) | → | b0(b0(a0(b1(a2(a5(a3(b7(a6(x1))))))))) | (183) |
a7(b7(b6(a4(b1(b2(a4(x1))))))) | → | b7(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) | (184) |
a3(b7(b6(a4(b1(b2(a4(x1))))))) | → | b3(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) | (185) |
a5(b3(b6(a4(b1(b2(a4(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) | (186) |
a1(b3(b6(a4(b1(b2(a4(x1))))))) | → | b1(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) | (187) |
a6(b5(b2(a4(b1(b2(a4(x1))))))) | → | b6(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) | (188) |
a2(b5(b2(a4(b1(b2(a4(x1))))))) | → | b2(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) | (189) |
a0(b1(b2(a4(b1(b2(a4(x1))))))) | → | b0(b0(a0(b1(a2(a5(b3(b6(a4(x1))))))))) | (190) |
a7(b7(b6(a4(a1(a3(b7(x1))))))) | → | b7(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) | (191) |
a3(b7(b6(a4(a1(a3(b7(x1))))))) | → | b3(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) | (192) |
a5(b3(b6(a4(a1(a3(b7(x1))))))) | → | b5(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) | (193) |
a1(b3(b6(a4(a1(a3(b7(x1))))))) | → | b1(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) | (194) |
a6(b5(b2(a4(a1(a3(b7(x1))))))) | → | b6(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) | (195) |
a2(b5(b2(a4(a1(a3(b7(x1))))))) | → | b2(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) | (196) |
a0(b1(b2(a4(a1(a3(b7(x1))))))) | → | b0(b0(a0(b1(a2(a5(a3(a7(b7(x1))))))))) | (197) |
a7(b7(b6(a4(b1(a2(b5(x1))))))) | → | b7(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) | (198) |
a3(b7(b6(a4(b1(a2(b5(x1))))))) | → | b3(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) | (199) |
a5(b3(b6(a4(b1(a2(b5(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) | (200) |
a1(b3(b6(a4(b1(a2(b5(x1))))))) | → | b1(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) | (201) |
a6(b5(b2(a4(b1(a2(b5(x1))))))) | → | b6(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) | (202) |
a2(b5(b2(a4(b1(a2(b5(x1))))))) | → | b2(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) | (203) |
a0(b1(b2(a4(b1(a2(b5(x1))))))) | → | b0(b0(a0(b1(a2(a5(b3(a6(b5(x1))))))))) | (204) |
a7(b7(b6(a4(a1(b3(b6(x1))))))) | → | b7(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) | (205) |
a3(b7(b6(a4(a1(b3(b6(x1))))))) | → | b3(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) | (206) |
a5(b3(b6(a4(a1(b3(b6(x1))))))) | → | b5(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) | (207) |
a1(b3(b6(a4(a1(b3(b6(x1))))))) | → | b1(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) | (208) |
a6(b5(b2(a4(a1(b3(b6(x1))))))) | → | b6(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) | (209) |
a2(b5(b2(a4(a1(b3(b6(x1))))))) | → | b2(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) | (210) |
a0(b1(b2(a4(a1(b3(b6(x1))))))) | → | b0(b0(a0(b1(a2(a5(a3(b7(b6(x1))))))))) | (211) |
a7(b7(b6(a4(b1(b2(b4(x1))))))) | → | b7(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) | (212) |
a3(b7(b6(a4(b1(b2(b4(x1))))))) | → | b3(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) | (213) |
a5(b3(b6(a4(b1(b2(b4(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) | (214) |
a1(b3(b6(a4(b1(b2(b4(x1))))))) | → | b1(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) | (215) |
a6(b5(b2(a4(b1(b2(b4(x1))))))) | → | b6(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) | (216) |
a2(b5(b2(a4(b1(b2(b4(x1))))))) | → | b2(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) | (217) |
a0(b1(b2(a4(b1(b2(b4(x1))))))) | → | b0(b0(a0(b1(a2(a5(b3(b6(b4(x1))))))))) | (218) |
[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)] | = |
|
a6(a5(b3(a6(a5(x1))))) | → | b6(a4(a1(x1))) | (159) |
a2(a5(b3(a6(a5(x1))))) | → | b2(a4(a1(x1))) | (160) |
a6(a5(b3(a6(b5(x1))))) | → | b6(a4(b1(x1))) | (161) |
a2(a5(b3(a6(b5(x1))))) | → | b2(a4(b1(x1))) | (162) |
a0(b1(b2(a4(a1(a3(a7(x1))))))) | → | b0(b0(a0(b1(a2(a5(a3(a7(a7(x1))))))))) | (169) |
a0(b1(b2(a4(b1(a2(a5(x1))))))) | → | b0(b0(a0(b1(a2(a5(b3(a6(a5(x1))))))))) | (176) |
a0(b1(b2(a4(a1(b3(a6(x1))))))) | → | b0(b0(a0(b1(a2(a5(a3(b7(a6(x1))))))))) | (183) |
a0(b1(b2(a4(b1(b2(a4(x1))))))) | → | b0(b0(a0(b1(a2(a5(b3(b6(a4(x1))))))))) | (190) |
a0(b1(b2(a4(a1(a3(b7(x1))))))) | → | b0(b0(a0(b1(a2(a5(a3(a7(b7(x1))))))))) | (197) |
a0(b1(b2(a4(b1(a2(b5(x1))))))) | → | b0(b0(a0(b1(a2(a5(b3(a6(b5(x1))))))))) | (204) |
a0(b1(b2(a4(a1(b3(b6(x1))))))) | → | b0(b0(a0(b1(a2(a5(a3(b7(b6(x1))))))))) | (211) |
a0(b1(b2(a4(b1(b2(b4(x1))))))) | → | b0(b0(a0(b1(a2(a5(b3(b6(b4(x1))))))))) | (218) |
[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 +
|
a7(b7(b6(a4(a1(a3(a7(x1))))))) | → | b7(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) | (163) |
a3(b7(b6(a4(a1(a3(a7(x1))))))) | → | b3(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) | (164) |
a5(b3(b6(a4(a1(a3(a7(x1))))))) | → | b5(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) | (165) |
a1(b3(b6(a4(a1(a3(a7(x1))))))) | → | b1(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) | (166) |
a6(b5(b2(a4(a1(a3(a7(x1))))))) | → | b6(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) | (167) |
a2(b5(b2(a4(a1(a3(a7(x1))))))) | → | b2(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) | (168) |
a7(b7(b6(a4(b1(a2(a5(x1))))))) | → | b7(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) | (170) |
a3(b7(b6(a4(b1(a2(a5(x1))))))) | → | b3(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) | (171) |
a5(b3(b6(a4(b1(a2(a5(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) | (172) |
a1(b3(b6(a4(b1(a2(a5(x1))))))) | → | b1(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) | (173) |
a6(b5(b2(a4(b1(a2(a5(x1))))))) | → | b6(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) | (174) |
a2(b5(b2(a4(b1(a2(a5(x1))))))) | → | b2(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) | (175) |
a7(b7(b6(a4(a1(b3(a6(x1))))))) | → | b7(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) | (177) |
a3(b7(b6(a4(a1(b3(a6(x1))))))) | → | b3(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) | (178) |
a5(b3(b6(a4(a1(b3(a6(x1))))))) | → | b5(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) | (179) |
a1(b3(b6(a4(a1(b3(a6(x1))))))) | → | b1(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) | (180) |
a6(b5(b2(a4(a1(b3(a6(x1))))))) | → | b6(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) | (181) |
a2(b5(b2(a4(a1(b3(a6(x1))))))) | → | b2(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) | (182) |
a7(b7(b6(a4(b1(b2(a4(x1))))))) | → | b7(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) | (184) |
a3(b7(b6(a4(b1(b2(a4(x1))))))) | → | b3(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) | (185) |
a1(b3(b6(a4(b1(b2(a4(x1))))))) | → | b1(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) | (187) |
a6(b5(b2(a4(b1(b2(a4(x1))))))) | → | b6(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) | (188) |
a2(b5(b2(a4(b1(b2(a4(x1))))))) | → | b2(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) | (189) |
a7(b7(b6(a4(a1(a3(b7(x1))))))) | → | b7(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) | (191) |
a3(b7(b6(a4(a1(a3(b7(x1))))))) | → | b3(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) | (192) |
a5(b3(b6(a4(a1(a3(b7(x1))))))) | → | b5(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) | (193) |
a1(b3(b6(a4(a1(a3(b7(x1))))))) | → | b1(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) | (194) |
a6(b5(b2(a4(a1(a3(b7(x1))))))) | → | b6(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) | (195) |
a2(b5(b2(a4(a1(a3(b7(x1))))))) | → | b2(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) | (196) |
a7(b7(b6(a4(b1(a2(b5(x1))))))) | → | b7(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) | (198) |
a3(b7(b6(a4(b1(a2(b5(x1))))))) | → | b3(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) | (199) |
a5(b3(b6(a4(b1(a2(b5(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) | (200) |
a1(b3(b6(a4(b1(a2(b5(x1))))))) | → | b1(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) | (201) |
a6(b5(b2(a4(b1(a2(b5(x1))))))) | → | b6(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) | (202) |
a2(b5(b2(a4(b1(a2(b5(x1))))))) | → | b2(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) | (203) |
a7(b7(b6(a4(a1(b3(b6(x1))))))) | → | b7(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) | (205) |
a3(b7(b6(a4(a1(b3(b6(x1))))))) | → | b3(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) | (206) |
a5(b3(b6(a4(a1(b3(b6(x1))))))) | → | b5(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) | (207) |
a1(b3(b6(a4(a1(b3(b6(x1))))))) | → | b1(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) | (208) |
a6(b5(b2(a4(a1(b3(b6(x1))))))) | → | b6(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) | (209) |
a2(b5(b2(a4(a1(b3(b6(x1))))))) | → | b2(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) | (210) |
a7(b7(b6(a4(b1(b2(b4(x1))))))) | → | b7(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) | (212) |
a3(b7(b6(a4(b1(b2(b4(x1))))))) | → | b3(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) | (213) |
a1(b3(b6(a4(b1(b2(b4(x1))))))) | → | b1(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) | (215) |
a6(b5(b2(a4(b1(b2(b4(x1))))))) | → | b6(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) | (216) |
a2(b5(b2(a4(b1(b2(b4(x1))))))) | → | b2(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) | (217) |
a4(b2(b1(a4(b6(b3(a5(x1))))))) | → | a4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) | (121) |
b4(b2(b1(a4(b6(b3(a5(x1))))))) | → | b4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) | (153) |
There are no rules in the TRS. Hence, it is terminating.
{b(☐), a(☐)}
We obtain the transformed TRSb(a(b(b(a(x1))))) | → | b(a(a(b(a(b(b(x1))))))) | (5) |
a(a(b(b(a(x1))))) | → | a(a(a(b(a(b(b(x1))))))) | (6) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(a(b(b(a(x1)))))) | → | b(b(a(a(b(a(b(b(x1)))))))) | (11) |
b(a(a(b(b(a(x1)))))) | → | b(a(a(a(b(a(b(b(x1)))))))) | (12) |
a(b(a(b(b(a(x1)))))) | → | a(b(a(a(b(a(b(b(x1)))))))) | (13) |
a(a(a(b(b(a(x1)))))) | → | a(a(a(a(b(a(b(b(x1)))))))) | (14) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(b(a(b(b(a(x1))))))) | → | b(b(b(a(a(b(a(b(b(x1))))))))) | (23) |
b(b(a(a(b(b(a(x1))))))) | → | b(b(a(a(a(b(a(b(b(x1))))))))) | (24) |
b(a(b(a(b(b(a(x1))))))) | → | b(a(b(a(a(b(a(b(b(x1))))))))) | (25) |
b(a(a(a(b(b(a(x1))))))) | → | b(a(a(a(a(b(a(b(b(x1))))))))) | (26) |
a(b(b(a(b(b(a(x1))))))) | → | a(b(b(a(a(b(a(b(b(x1))))))))) | (27) |
a(b(a(a(b(b(a(x1))))))) | → | a(b(a(a(a(b(a(b(b(x1))))))))) | (28) |
a(a(b(a(b(b(a(x1))))))) | → | a(a(b(a(a(b(a(b(b(x1))))))))) | (29) |
a(a(a(a(b(b(a(x1))))))) | → | a(a(a(a(a(b(a(b(b(x1))))))))) | (30) |
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 |
a7(a3(a1(a4(b6(b7(a7(x1))))))) | → | a7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) | (95) |
a7(a3(a1(a4(b6(b7(a3(x1))))))) | → | a7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) | (96) |
a7(a3(a1(a4(b6(b3(a5(x1))))))) | → | a7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) | (97) |
a7(a3(a1(a4(b6(b3(a1(x1))))))) | → | a7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) | (98) |
a7(a3(a1(a4(b2(b5(a6(x1))))))) | → | a7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) | (99) |
a7(a3(a1(a4(b2(b5(a2(x1))))))) | → | a7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) | (100) |
a7(a3(a1(a4(b2(b1(a4(x1))))))) | → | a7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (101) |
a7(a3(a1(a4(b2(b1(a0(x1))))))) | → | a7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) | (102) |
a5(a2(b1(a4(b6(b7(a7(x1))))))) | → | a5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) | (103) |
a5(a2(b1(a4(b6(b7(a3(x1))))))) | → | a5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) | (104) |
a5(a2(b1(a4(b6(b3(a5(x1))))))) | → | a5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) | (105) |
a5(a2(b1(a4(b6(b3(a1(x1))))))) | → | a5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) | (106) |
a5(a2(b1(a4(b2(b5(a6(x1))))))) | → | a5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) | (107) |
a5(a2(b1(a4(b2(b5(a2(x1))))))) | → | a5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) | (108) |
a5(a2(b1(a4(b2(b1(a4(x1))))))) | → | a5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (109) |
a5(a2(b1(a4(b2(b1(a0(x1))))))) | → | a5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) | (110) |
a6(b3(a1(a4(b6(b7(a7(x1))))))) | → | a6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) | (111) |
a6(b3(a1(a4(b6(b7(a3(x1))))))) | → | a6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) | (112) |
a6(b3(a1(a4(b6(b3(a5(x1))))))) | → | a6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) | (113) |
a6(b3(a1(a4(b6(b3(a1(x1))))))) | → | a6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) | (114) |
a6(b3(a1(a4(b2(b5(a6(x1))))))) | → | a6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) | (115) |
a6(b3(a1(a4(b2(b5(a2(x1))))))) | → | a6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) | (116) |
a6(b3(a1(a4(b2(b1(a4(x1))))))) | → | a6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (117) |
a6(b3(a1(a4(b2(b1(a0(x1))))))) | → | a6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) | (118) |
a4(b2(b1(a4(b6(b7(a7(x1))))))) | → | a4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) | (119) |
a4(b2(b1(a4(b6(b7(a3(x1))))))) | → | a4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) | (120) |
a4(b2(b1(a4(b6(b3(a5(x1))))))) | → | a4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) | (121) |
a4(b2(b1(a4(b6(b3(a1(x1))))))) | → | a4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) | (122) |
a4(b2(b1(a4(b2(b5(a6(x1))))))) | → | a4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) | (123) |
a4(b2(b1(a4(b2(b5(a2(x1))))))) | → | a4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) | (124) |
a4(b2(b1(a4(b2(b1(a4(x1))))))) | → | a4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (125) |
a4(b2(b1(a4(b2(b1(a0(x1))))))) | → | a4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) | (126) |
b7(a3(a1(a4(b6(b7(a7(x1))))))) | → | b7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) | (127) |
b7(a3(a1(a4(b6(b7(a3(x1))))))) | → | b7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) | (128) |
b7(a3(a1(a4(b6(b3(a5(x1))))))) | → | b7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) | (129) |
b7(a3(a1(a4(b6(b3(a1(x1))))))) | → | b7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) | (130) |
b7(a3(a1(a4(b2(b5(a6(x1))))))) | → | b7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) | (131) |
b7(a3(a1(a4(b2(b5(a2(x1))))))) | → | b7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) | (132) |
b7(a3(a1(a4(b2(b1(a4(x1))))))) | → | b7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (133) |
b7(a3(a1(a4(b2(b1(a0(x1))))))) | → | b7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) | (134) |
b5(a2(b1(a4(b6(b7(a7(x1))))))) | → | b5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) | (135) |
b5(a2(b1(a4(b6(b7(a3(x1))))))) | → | b5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) | (136) |
b5(a2(b1(a4(b6(b3(a5(x1))))))) | → | b5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) | (137) |
b5(a2(b1(a4(b6(b3(a1(x1))))))) | → | b5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) | (138) |
b5(a2(b1(a4(b2(b5(a6(x1))))))) | → | b5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) | (139) |
b5(a2(b1(a4(b2(b5(a2(x1))))))) | → | b5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) | (140) |
b5(a2(b1(a4(b2(b1(a4(x1))))))) | → | b5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (141) |
b5(a2(b1(a4(b2(b1(a0(x1))))))) | → | b5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) | (142) |
b6(b3(a1(a4(b6(b7(a7(x1))))))) | → | b6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) | (143) |
b6(b3(a1(a4(b6(b7(a3(x1))))))) | → | b6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) | (144) |
b6(b3(a1(a4(b6(b3(a5(x1))))))) | → | b6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) | (145) |
b6(b3(a1(a4(b6(b3(a1(x1))))))) | → | b6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) | (146) |
b6(b3(a1(a4(b2(b5(a6(x1))))))) | → | b6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) | (147) |
b6(b3(a1(a4(b2(b5(a2(x1))))))) | → | b6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) | (148) |
b6(b3(a1(a4(b2(b1(a4(x1))))))) | → | b6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (149) |
b6(b3(a1(a4(b2(b1(a0(x1))))))) | → | b6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) | (150) |
b4(b2(b1(a4(b6(b7(a7(x1))))))) | → | b4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) | (151) |
b4(b2(b1(a4(b6(b7(a3(x1))))))) | → | b4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) | (152) |
b4(b2(b1(a4(b6(b3(a5(x1))))))) | → | b4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) | (153) |
b4(b2(b1(a4(b6(b3(a1(x1))))))) | → | b4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) | (154) |
b4(b2(b1(a4(b2(b5(a6(x1))))))) | → | b4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) | (155) |
b4(b2(b1(a4(b2(b5(a2(x1))))))) | → | b4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) | (156) |
b4(b2(b1(a4(b2(b1(a4(x1))))))) | → | b4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (157) |
b4(b2(b1(a4(b2(b1(a0(x1))))))) | → | b4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) | (158) |
[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 +
|
a7(a3(a1(a4(b6(b7(a7(x1))))))) | → | a7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) | (95) |
a7(a3(a1(a4(b6(b7(a3(x1))))))) | → | a7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) | (96) |
a7(a3(a1(a4(b6(b3(a5(x1))))))) | → | a7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) | (97) |
a7(a3(a1(a4(b6(b3(a1(x1))))))) | → | a7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) | (98) |
a7(a3(a1(a4(b2(b5(a6(x1))))))) | → | a7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) | (99) |
a7(a3(a1(a4(b2(b5(a2(x1))))))) | → | a7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) | (100) |
a7(a3(a1(a4(b2(b1(a4(x1))))))) | → | a7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (101) |
a7(a3(a1(a4(b2(b1(a0(x1))))))) | → | a7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) | (102) |
a5(a2(b1(a4(b6(b7(a7(x1))))))) | → | a5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) | (103) |
a5(a2(b1(a4(b6(b7(a3(x1))))))) | → | a5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) | (104) |
a5(a2(b1(a4(b6(b3(a5(x1))))))) | → | a5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) | (105) |
a5(a2(b1(a4(b6(b3(a1(x1))))))) | → | a5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) | (106) |
a5(a2(b1(a4(b2(b5(a6(x1))))))) | → | a5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) | (107) |
a5(a2(b1(a4(b2(b5(a2(x1))))))) | → | a5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) | (108) |
a5(a2(b1(a4(b2(b1(a4(x1))))))) | → | a5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (109) |
a5(a2(b1(a4(b2(b1(a0(x1))))))) | → | a5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) | (110) |
a6(b3(a1(a4(b6(b7(a7(x1))))))) | → | a6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) | (111) |
a6(b3(a1(a4(b6(b7(a3(x1))))))) | → | a6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) | (112) |
a6(b3(a1(a4(b6(b3(a5(x1))))))) | → | a6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) | (113) |
a6(b3(a1(a4(b6(b3(a1(x1))))))) | → | a6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) | (114) |
a6(b3(a1(a4(b2(b5(a6(x1))))))) | → | a6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) | (115) |
a6(b3(a1(a4(b2(b5(a2(x1))))))) | → | a6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) | (116) |
a6(b3(a1(a4(b2(b1(a4(x1))))))) | → | a6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (117) |
a6(b3(a1(a4(b2(b1(a0(x1))))))) | → | a6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) | (118) |
a4(b2(b1(a4(b6(b7(a7(x1))))))) | → | a4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) | (119) |
a4(b2(b1(a4(b6(b7(a3(x1))))))) | → | a4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) | (120) |
a4(b2(b1(a4(b6(b3(a1(x1))))))) | → | a4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) | (122) |
a4(b2(b1(a4(b2(b5(a6(x1))))))) | → | a4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) | (123) |
a4(b2(b1(a4(b2(b5(a2(x1))))))) | → | a4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) | (124) |
a4(b2(b1(a4(b2(b1(a4(x1))))))) | → | a4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (125) |
a4(b2(b1(a4(b2(b1(a0(x1))))))) | → | a4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) | (126) |
b7(a3(a1(a4(b6(b7(a7(x1))))))) | → | b7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) | (127) |
b7(a3(a1(a4(b6(b7(a3(x1))))))) | → | b7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) | (128) |
b7(a3(a1(a4(b6(b3(a5(x1))))))) | → | b7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) | (129) |
b7(a3(a1(a4(b6(b3(a1(x1))))))) | → | b7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) | (130) |
b7(a3(a1(a4(b2(b5(a6(x1))))))) | → | b7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) | (131) |
b7(a3(a1(a4(b2(b5(a2(x1))))))) | → | b7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) | (132) |
b7(a3(a1(a4(b2(b1(a4(x1))))))) | → | b7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (133) |
b7(a3(a1(a4(b2(b1(a0(x1))))))) | → | b7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) | (134) |
b5(a2(b1(a4(b6(b7(a7(x1))))))) | → | b5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) | (135) |
b5(a2(b1(a4(b6(b7(a3(x1))))))) | → | b5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) | (136) |
b5(a2(b1(a4(b6(b3(a5(x1))))))) | → | b5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) | (137) |
b5(a2(b1(a4(b6(b3(a1(x1))))))) | → | b5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) | (138) |
b5(a2(b1(a4(b2(b5(a6(x1))))))) | → | b5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) | (139) |
b5(a2(b1(a4(b2(b5(a2(x1))))))) | → | b5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) | (140) |
b5(a2(b1(a4(b2(b1(a4(x1))))))) | → | b5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (141) |
b5(a2(b1(a4(b2(b1(a0(x1))))))) | → | b5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) | (142) |
b6(b3(a1(a4(b6(b7(a7(x1))))))) | → | b6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) | (143) |
b6(b3(a1(a4(b6(b7(a3(x1))))))) | → | b6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) | (144) |
b6(b3(a1(a4(b6(b3(a5(x1))))))) | → | b6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) | (145) |
b6(b3(a1(a4(b6(b3(a1(x1))))))) | → | b6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) | (146) |
b6(b3(a1(a4(b2(b5(a6(x1))))))) | → | b6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) | (147) |
b6(b3(a1(a4(b2(b5(a2(x1))))))) | → | b6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) | (148) |
b6(b3(a1(a4(b2(b1(a4(x1))))))) | → | b6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) | (149) |
b6(b3(a1(a4(b2(b1(a0(x1))))))) | → | b6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) | (150) |
b4(b2(b1(a4(b6(b7(a7(x1))))))) | → | b4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) | (151) |
b4(b2(b1(a4(b6(b7(a3(x1))))))) | → | b4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) | (152) |
b4(b2(b1(a4(b6(b3(a1(x1))))))) | → | b4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) | (154) |
b4(b2(b1(a4(b2(b5(a6(x1))))))) | → | b4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) | (155) |
b4(b2(b1(a4(b2(b5(a2(x1))))))) | → | b4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) | (156) |
b4(b2(b1(a4(b2(b1(a4(x1))))))) | → | b4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) | (157) |
b4(b2(b1(a4(b2(b1(a0(x1))))))) | → | b4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) | (158) |
a5(b3(b6(a4(b1(b2(a4(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) | (186) |
a5(b3(b6(a4(b1(b2(b4(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) | (214) |
[b4(x1)] | = |
|
||||||||
[b2(x1)] | = |
|
||||||||
[b6(x1)] | = |
|
||||||||
[b1(x1)] | = |
|
||||||||
[b5(x1)] | = |
|
||||||||
[b3(x1)] | = |
|
||||||||
[a4(x1)] | = |
|
||||||||
[a2(x1)] | = |
|
||||||||
[a5(x1)] | = |
|
a5(b3(b6(a4(b1(b2(a4(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) | (186) |
a5(b3(b6(a4(b1(b2(b4(x1))))))) | → | b5(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) | (214) |
There are no rules.
There are no rules in the TRS. Hence, it is terminating.