The rewrite relation of the following TRS is considered.
b(a(b(b(a(b(x1)))))) | → | a(b(a(b(b(b(a(x1))))))) | (1) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(a(b(b(a(b(x1))))))) | → | b(a(b(a(b(b(b(a(x1)))))))) | (2) |
a(b(a(b(b(a(b(x1))))))) | → | a(a(b(a(b(b(b(a(x1)))))))) | (3) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(b(a(b(b(a(b(x1)))))))) | → | b(b(a(b(a(b(b(b(a(x1))))))))) | (4) |
b(a(b(a(b(b(a(b(x1)))))))) | → | b(a(a(b(a(b(b(b(a(x1))))))))) | (5) |
a(b(b(a(b(b(a(b(x1)))))))) | → | a(b(a(b(a(b(b(b(a(x1))))))))) | (6) |
a(a(b(a(b(b(a(b(x1)))))))) | → | a(a(a(b(a(b(b(b(a(x1))))))))) | (7) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(b(b(a(b(b(a(b(x1))))))))) | → | b(b(b(a(b(a(b(b(b(a(x1)))))))))) | (8) |
b(b(a(b(a(b(b(a(b(x1))))))))) | → | b(b(a(a(b(a(b(b(b(a(x1)))))))))) | (9) |
b(a(b(b(a(b(b(a(b(x1))))))))) | → | b(a(b(a(b(a(b(b(b(a(x1)))))))))) | (10) |
b(a(a(b(a(b(b(a(b(x1))))))))) | → | b(a(a(a(b(a(b(b(b(a(x1)))))))))) | (11) |
a(b(b(b(a(b(b(a(b(x1))))))))) | → | a(b(b(a(b(a(b(b(b(a(x1)))))))))) | (12) |
a(b(a(b(a(b(b(a(b(x1))))))))) | → | a(b(a(a(b(a(b(b(b(a(x1)))))))))) | (13) |
a(a(b(b(a(b(b(a(b(x1))))))))) | → | a(a(b(a(b(a(b(b(b(a(x1)))))))))) | (14) |
a(a(a(b(a(b(b(a(b(x1))))))))) | → | a(a(a(a(b(a(b(b(b(a(x1)))))))))) | (15) |
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 |
b0(b4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (16) |
b0(b4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (17) |
b0(b4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (18) |
b0(b4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (19) |
b0(b4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (20) |
b0(b4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (21) |
b0(b4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (22) |
b0(b4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (23) |
b2(b5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (24) |
b2(b5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (25) |
b2(b5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (26) |
b2(b5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (27) |
b2(b5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (28) |
b2(b5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (29) |
b2(b5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (30) |
b2(b5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (31) |
b1(a4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (32) |
b1(a4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (33) |
b1(a4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (34) |
b1(a4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (35) |
b1(a4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (36) |
b1(a4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (37) |
b1(a4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (38) |
b1(a4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (39) |
b3(a5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (40) |
b3(a5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (41) |
b3(a5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (42) |
b3(a5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (43) |
b3(a5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (44) |
b3(a5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (45) |
b3(a5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (46) |
b3(a5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (47) |
a0(b4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (48) |
a0(b4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (49) |
a0(b4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (50) |
a0(b4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (51) |
a0(b4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (52) |
a0(b4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (53) |
a0(b4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (54) |
a0(b4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (55) |
a2(b5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (56) |
a2(b5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (57) |
a2(b5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (58) |
a2(b5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (59) |
a2(b5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (60) |
a2(b5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (61) |
a2(b5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (62) |
a2(b5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (63) |
a1(a4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (64) |
a1(a4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (65) |
a1(a4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (66) |
a1(a4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (67) |
a1(a4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (68) |
a1(a4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (69) |
a1(a4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (70) |
a1(a4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (71) |
a3(a5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (72) |
a3(a5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (73) |
a3(a5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (74) |
a3(a5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (75) |
a3(a5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (76) |
a3(a5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (77) |
a3(a5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (78) |
a3(a5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (79) |
[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 +
|
b0(b4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (16) |
b0(b4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (17) |
b0(b4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (18) |
b0(b4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (19) |
b0(b4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (20) |
b0(b4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (21) |
b0(b4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (22) |
b0(b4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | b4(b2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (23) |
b2(b5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (24) |
b2(b5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (25) |
b2(b5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (26) |
b2(b5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (27) |
b2(b5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (28) |
b2(b5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (29) |
b2(b5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (30) |
b2(b5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | b6(b3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (31) |
b1(a4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (32) |
b1(a4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (33) |
b1(a4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (34) |
b1(a4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (35) |
b1(a4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (36) |
b1(a4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (37) |
b1(a4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (38) |
b1(a4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | b5(a2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (39) |
b3(a5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (40) |
b3(a5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (41) |
b3(a5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (42) |
b3(a5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (43) |
b3(a5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (44) |
b3(a5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (45) |
b3(a5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (46) |
b3(a5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | b7(a3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (47) |
a0(b4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (48) |
a0(b4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (49) |
a0(b4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (50) |
a0(b4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (51) |
a0(b4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (52) |
a0(b4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (53) |
a0(b4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (54) |
a0(b4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | a4(b2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (55) |
a2(b5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (56) |
a2(b5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (57) |
a2(b5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (58) |
a2(b5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (59) |
a2(b5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (60) |
a2(b5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (61) |
a2(b5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (62) |
a2(b5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | a6(b3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (63) |
a1(a4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (64) |
a1(a4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) | (65) |
a1(a4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (66) |
a1(a4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (67) |
a1(a4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (68) |
a1(a4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (69) |
a1(a4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (70) |
a1(a4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | a5(a2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (71) |
a3(a5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) | (72) |
a3(a5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) | (74) |
a3(a5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) | (75) |
a3(a5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) | (76) |
a3(a5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) | (77) |
a3(a5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) | (78) |
a3(a5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) | → | a7(a3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) | (79) |
b4(a0(b1(b2(a4(b1(a2(a5(a3(x1))))))))) | → | a4(b1(b2(b4(a0(b1(a2(a5(a3(a7(x1)))))))))) | (80) |
[b4(x1)] | = |
|
||||||||
[b2(x1)] | = |
|
||||||||
[b1(x1)] | = |
|
||||||||
[a0(x1)] | = |
|
||||||||
[a4(x1)] | = |
|
||||||||
[a2(x1)] | = |
|
||||||||
[a5(x1)] | = |
|
||||||||
[a3(x1)] | = |
|
||||||||
[a7(x1)] | = |
|
b4(a0(b1(b2(a4(b1(a2(a5(a3(x1))))))))) | → | a4(b1(b2(b4(a0(b1(a2(a5(a3(a7(x1)))))))))) | (80) |
There are no rules.
There are no rules in the TRS. Hence, it is terminating.