The rewrite relation of the following TRS is considered.
b(a(b(b(x1)))) | → | b(b(a(a(x1)))) | (1) |
a(a(b(b(x1)))) | → | a(b(a(a(x1)))) | (2) |
b(b(b(b(x1)))) | → | b(a(a(a(x1)))) | (3) |
a(b(a(a(x1)))) | → | a(b(b(a(x1)))) | (4) |
We split R in the relative problem D/R-D and R-D, where the rules D
b(b(b(b(x1)))) | → | b(a(a(a(x1)))) | (3) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(b(b(b(x1))))) | → | b(b(a(a(a(x1))))) | (5) |
a(b(b(b(b(x1))))) | → | a(b(a(a(a(x1))))) | (6) |
b(b(a(b(b(x1))))) | → | b(b(b(a(a(x1))))) | (7) |
b(a(a(b(b(x1))))) | → | b(a(b(a(a(x1))))) | (8) |
b(a(b(a(a(x1))))) | → | b(a(b(b(a(x1))))) | (9) |
a(b(a(b(b(x1))))) | → | a(b(b(a(a(x1))))) | (10) |
a(a(a(b(b(x1))))) | → | a(a(b(a(a(x1))))) | (11) |
a(a(b(a(a(x1))))) | → | a(a(b(b(a(x1))))) | (12) |
{b(☐), a(☐)}
We obtain the transformed TRSb(b(b(b(b(b(x1)))))) | → | b(b(b(a(a(a(x1)))))) | (13) |
b(a(b(b(b(b(x1)))))) | → | b(a(b(a(a(a(x1)))))) | (14) |
a(b(b(b(b(b(x1)))))) | → | a(b(b(a(a(a(x1)))))) | (15) |
a(a(b(b(b(b(x1)))))) | → | a(a(b(a(a(a(x1)))))) | (16) |
b(b(b(a(b(b(x1)))))) | → | b(b(b(b(a(a(x1)))))) | (17) |
b(b(a(a(b(b(x1)))))) | → | b(b(a(b(a(a(x1)))))) | (18) |
b(b(a(b(a(a(x1)))))) | → | b(b(a(b(b(a(x1)))))) | (19) |
b(a(b(a(b(b(x1)))))) | → | b(a(b(b(a(a(x1)))))) | (20) |
b(a(a(a(b(b(x1)))))) | → | b(a(a(b(a(a(x1)))))) | (21) |
b(a(a(b(a(a(x1)))))) | → | b(a(a(b(b(a(x1)))))) | (22) |
a(b(b(a(b(b(x1)))))) | → | a(b(b(b(a(a(x1)))))) | (23) |
a(b(a(a(b(b(x1)))))) | → | a(b(a(b(a(a(x1)))))) | (24) |
a(b(a(b(a(a(x1)))))) | → | a(b(a(b(b(a(x1)))))) | (25) |
a(a(b(a(b(b(x1)))))) | → | a(a(b(b(a(a(x1)))))) | (26) |
a(a(a(a(b(b(x1)))))) | → | a(a(a(b(a(a(x1)))))) | (27) |
a(a(a(b(a(a(x1)))))) | → | a(a(a(b(b(a(x1)))))) | (28) |
As carrier we take the set {0,...,3}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 4):
[b(x1)] | = | 2x1 + 0 |
[a(x1)] | = | 2x1 + 1 |
b0(b0(b0(b0(b0(b0(x1)))))) | → | b0(b2(b3(a3(a1(a0(x1)))))) | (29) |
b0(b0(b0(b0(b0(b2(x1)))))) | → | b0(b2(b3(a3(a1(a2(x1)))))) | (30) |
b0(b0(b0(b0(b2(b1(x1)))))) | → | b0(b2(b3(a3(a3(a1(x1)))))) | (31) |
b0(b0(b0(b0(b2(b3(x1)))))) | → | b0(b2(b3(a3(a3(a3(x1)))))) | (32) |
b1(a0(b0(b0(b0(b0(x1)))))) | → | b1(a2(b3(a3(a1(a0(x1)))))) | (33) |
b1(a0(b0(b0(b0(b2(x1)))))) | → | b1(a2(b3(a3(a1(a2(x1)))))) | (34) |
b1(a0(b0(b0(b2(b1(x1)))))) | → | b1(a2(b3(a3(a3(a1(x1)))))) | (35) |
b1(a0(b0(b0(b2(b3(x1)))))) | → | b1(a2(b3(a3(a3(a3(x1)))))) | (36) |
a0(b0(b0(b0(b0(b0(x1)))))) | → | a0(b2(b3(a3(a1(a0(x1)))))) | (37) |
a0(b0(b0(b0(b0(b2(x1)))))) | → | a0(b2(b3(a3(a1(a2(x1)))))) | (38) |
a0(b0(b0(b0(b2(b1(x1)))))) | → | a0(b2(b3(a3(a3(a1(x1)))))) | (39) |
a0(b0(b0(b0(b2(b3(x1)))))) | → | a0(b2(b3(a3(a3(a3(x1)))))) | (40) |
a1(a0(b0(b0(b0(b0(x1)))))) | → | a1(a2(b3(a3(a1(a0(x1)))))) | (41) |
a1(a0(b0(b0(b0(b2(x1)))))) | → | a1(a2(b3(a3(a1(a2(x1)))))) | (42) |
a1(a0(b0(b0(b2(b1(x1)))))) | → | a1(a2(b3(a3(a3(a1(x1)))))) | (43) |
a1(a0(b0(b0(b2(b3(x1)))))) | → | a1(a2(b3(a3(a3(a3(x1)))))) | (44) |
b0(b2(b1(a0(b0(b0(x1)))))) | → | b0(b0(b2(b3(a1(a0(x1)))))) | (45) |
b0(b2(b1(a0(b0(b2(x1)))))) | → | b0(b0(b2(b3(a1(a2(x1)))))) | (46) |
b0(b2(b1(a0(b2(b1(x1)))))) | → | b0(b0(b2(b3(a3(a1(x1)))))) | (47) |
b0(b2(b1(a0(b2(b3(x1)))))) | → | b0(b0(b2(b3(a3(a3(x1)))))) | (48) |
b1(a2(b1(a0(b0(b0(x1)))))) | → | b1(a0(b2(b3(a1(a0(x1)))))) | (49) |
b1(a2(b1(a0(b0(b2(x1)))))) | → | b1(a0(b2(b3(a1(a2(x1)))))) | (50) |
b1(a2(b1(a0(b2(b1(x1)))))) | → | b1(a0(b2(b3(a3(a1(x1)))))) | (51) |
b1(a2(b1(a0(b2(b3(x1)))))) | → | b1(a0(b2(b3(a3(a3(x1)))))) | (52) |
a0(b2(b1(a0(b0(b0(x1)))))) | → | a0(b0(b2(b3(a1(a0(x1)))))) | (53) |
a0(b2(b1(a0(b0(b2(x1)))))) | → | a0(b0(b2(b3(a1(a2(x1)))))) | (54) |
a0(b2(b1(a0(b2(b1(x1)))))) | → | a0(b0(b2(b3(a3(a1(x1)))))) | (55) |
a0(b2(b1(a0(b2(b3(x1)))))) | → | a0(b0(b2(b3(a3(a3(x1)))))) | (56) |
a1(a2(b1(a0(b0(b0(x1)))))) | → | a1(a0(b2(b3(a1(a0(x1)))))) | (57) |
a1(a2(b1(a0(b0(b2(x1)))))) | → | a1(a0(b2(b3(a1(a2(x1)))))) | (58) |
a1(a2(b1(a0(b2(b1(x1)))))) | → | a1(a0(b2(b3(a3(a1(x1)))))) | (59) |
a1(a2(b1(a0(b2(b3(x1)))))) | → | a1(a0(b2(b3(a3(a3(x1)))))) | (60) |
b2(b3(a1(a0(b0(b0(x1)))))) | → | b2(b1(a2(b3(a1(a0(x1)))))) | (61) |
b2(b3(a1(a0(b0(b2(x1)))))) | → | b2(b1(a2(b3(a1(a2(x1)))))) | (62) |
b2(b3(a1(a0(b2(b1(x1)))))) | → | b2(b1(a2(b3(a3(a1(x1)))))) | (63) |
b2(b3(a1(a0(b2(b3(x1)))))) | → | b2(b1(a2(b3(a3(a3(x1)))))) | (64) |
b3(a3(a1(a0(b0(b0(x1)))))) | → | b3(a1(a2(b3(a1(a0(x1)))))) | (65) |
b3(a3(a1(a0(b0(b2(x1)))))) | → | b3(a1(a2(b3(a1(a2(x1)))))) | (66) |
b3(a3(a1(a0(b2(b1(x1)))))) | → | b3(a1(a2(b3(a3(a1(x1)))))) | (67) |
b3(a3(a1(a0(b2(b3(x1)))))) | → | b3(a1(a2(b3(a3(a3(x1)))))) | (68) |
a2(b3(a1(a0(b0(b0(x1)))))) | → | a2(b1(a2(b3(a1(a0(x1)))))) | (69) |
a2(b3(a1(a0(b0(b2(x1)))))) | → | a2(b1(a2(b3(a1(a2(x1)))))) | (70) |
a2(b3(a1(a0(b2(b1(x1)))))) | → | a2(b1(a2(b3(a3(a1(x1)))))) | (71) |
a2(b3(a1(a0(b2(b3(x1)))))) | → | a2(b1(a2(b3(a3(a3(x1)))))) | (72) |
a3(a3(a1(a0(b0(b0(x1)))))) | → | a3(a1(a2(b3(a1(a0(x1)))))) | (73) |
a3(a3(a1(a0(b0(b2(x1)))))) | → | a3(a1(a2(b3(a1(a2(x1)))))) | (74) |
a3(a3(a1(a0(b2(b1(x1)))))) | → | a3(a1(a2(b3(a3(a1(x1)))))) | (75) |
a3(a3(a1(a0(b2(b3(x1)))))) | → | a3(a1(a2(b3(a3(a3(x1)))))) | (76) |
b2(b1(a2(b3(a1(a0(x1)))))) | → | b2(b1(a0(b2(b1(a0(x1)))))) | (77) |
b2(b1(a2(b3(a1(a2(x1)))))) | → | b2(b1(a0(b2(b1(a2(x1)))))) | (78) |
b2(b1(a2(b3(a3(a1(x1)))))) | → | b2(b1(a0(b2(b3(a1(x1)))))) | (79) |
b2(b1(a2(b3(a3(a3(x1)))))) | → | b2(b1(a0(b2(b3(a3(x1)))))) | (80) |
b3(a1(a2(b3(a1(a0(x1)))))) | → | b3(a1(a0(b2(b1(a0(x1)))))) | (81) |
b3(a1(a2(b3(a1(a2(x1)))))) | → | b3(a1(a0(b2(b1(a2(x1)))))) | (82) |
b3(a1(a2(b3(a3(a1(x1)))))) | → | b3(a1(a0(b2(b3(a1(x1)))))) | (83) |
b3(a1(a2(b3(a3(a3(x1)))))) | → | b3(a1(a0(b2(b3(a3(x1)))))) | (84) |
a2(b1(a2(b3(a1(a0(x1)))))) | → | a2(b1(a0(b2(b1(a0(x1)))))) | (85) |
a2(b1(a2(b3(a1(a2(x1)))))) | → | a2(b1(a0(b2(b1(a2(x1)))))) | (86) |
a2(b1(a2(b3(a3(a1(x1)))))) | → | a2(b1(a0(b2(b3(a1(x1)))))) | (87) |
a2(b1(a2(b3(a3(a3(x1)))))) | → | a2(b1(a0(b2(b3(a3(x1)))))) | (88) |
a3(a1(a2(b3(a1(a0(x1)))))) | → | a3(a1(a0(b2(b1(a0(x1)))))) | (89) |
a3(a1(a2(b3(a1(a2(x1)))))) | → | a3(a1(a0(b2(b1(a2(x1)))))) | (90) |
a3(a1(a2(b3(a3(a1(x1)))))) | → | a3(a1(a0(b2(b3(a1(x1)))))) | (91) |
a3(a1(a2(b3(a3(a3(x1)))))) | → | a3(a1(a0(b2(b3(a3(x1)))))) | (92) |
[b0(x1)] | = |
x1 +
|
||||
[b2(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[b3(x1)] | = |
x1 +
|
||||
[a0(x1)] | = |
x1 +
|
||||
[a2(x1)] | = |
x1 +
|
||||
[a1(x1)] | = |
x1 +
|
||||
[a3(x1)] | = |
x1 +
|
b0(b0(b0(b0(b0(b0(x1)))))) | → | b0(b2(b3(a3(a1(a0(x1)))))) | (29) |
b0(b0(b0(b0(b0(b2(x1)))))) | → | b0(b2(b3(a3(a1(a2(x1)))))) | (30) |
b0(b0(b0(b0(b2(b1(x1)))))) | → | b0(b2(b3(a3(a3(a1(x1)))))) | (31) |
b0(b0(b0(b0(b2(b3(x1)))))) | → | b0(b2(b3(a3(a3(a3(x1)))))) | (32) |
b1(a0(b0(b0(b0(b0(x1)))))) | → | b1(a2(b3(a3(a1(a0(x1)))))) | (33) |
b1(a0(b0(b0(b0(b2(x1)))))) | → | b1(a2(b3(a3(a1(a2(x1)))))) | (34) |
b1(a0(b0(b0(b2(b1(x1)))))) | → | b1(a2(b3(a3(a3(a1(x1)))))) | (35) |
b1(a0(b0(b0(b2(b3(x1)))))) | → | b1(a2(b3(a3(a3(a3(x1)))))) | (36) |
a0(b0(b0(b0(b0(b0(x1)))))) | → | a0(b2(b3(a3(a1(a0(x1)))))) | (37) |
a0(b0(b0(b0(b0(b2(x1)))))) | → | a0(b2(b3(a3(a1(a2(x1)))))) | (38) |
a0(b0(b0(b0(b2(b1(x1)))))) | → | a0(b2(b3(a3(a3(a1(x1)))))) | (39) |
a0(b0(b0(b0(b2(b3(x1)))))) | → | a0(b2(b3(a3(a3(a3(x1)))))) | (40) |
a1(a0(b0(b0(b0(b0(x1)))))) | → | a1(a2(b3(a3(a1(a0(x1)))))) | (41) |
a1(a0(b0(b0(b0(b2(x1)))))) | → | a1(a2(b3(a3(a1(a2(x1)))))) | (42) |
a1(a0(b0(b0(b2(b1(x1)))))) | → | a1(a2(b3(a3(a3(a1(x1)))))) | (43) |
a1(a0(b0(b0(b2(b3(x1)))))) | → | a1(a2(b3(a3(a3(a3(x1)))))) | (44) |
b0(b2(b1(a0(b0(b0(x1)))))) | → | b0(b0(b2(b3(a1(a0(x1)))))) | (45) |
b1(a2(b1(a0(b0(b0(x1)))))) | → | b1(a0(b2(b3(a1(a0(x1)))))) | (49) |
b1(a2(b1(a0(b0(b2(x1)))))) | → | b1(a0(b2(b3(a1(a2(x1)))))) | (50) |
b1(a2(b1(a0(b2(b1(x1)))))) | → | b1(a0(b2(b3(a3(a1(x1)))))) | (51) |
b1(a2(b1(a0(b2(b3(x1)))))) | → | b1(a0(b2(b3(a3(a3(x1)))))) | (52) |
a0(b2(b1(a0(b0(b0(x1)))))) | → | a0(b0(b2(b3(a1(a0(x1)))))) | (53) |
a1(a2(b1(a0(b0(b0(x1)))))) | → | a1(a0(b2(b3(a1(a0(x1)))))) | (57) |
a1(a2(b1(a0(b0(b2(x1)))))) | → | a1(a0(b2(b3(a1(a2(x1)))))) | (58) |
a1(a2(b1(a0(b2(b1(x1)))))) | → | a1(a0(b2(b3(a3(a1(x1)))))) | (59) |
a1(a2(b1(a0(b2(b3(x1)))))) | → | a1(a0(b2(b3(a3(a3(x1)))))) | (60) |
b2(b3(a1(a0(b0(b0(x1)))))) | → | b2(b1(a2(b3(a1(a0(x1)))))) | (61) |
b3(a3(a1(a0(b0(b0(x1)))))) | → | b3(a1(a2(b3(a1(a0(x1)))))) | (65) |
a2(b3(a1(a0(b0(b0(x1)))))) | → | a2(b1(a2(b3(a1(a0(x1)))))) | (69) |
a3(a3(a1(a0(b0(b0(x1)))))) | → | a3(a1(a2(b3(a1(a0(x1)))))) | (73) |
There are no rules in the TRS. Hence, it is terminating.
{b(☐), a(☐)}
We obtain the transformed TRSb(b(a(b(b(x1))))) | → | b(b(b(a(a(x1))))) | (7) |
b(a(a(b(b(x1))))) | → | b(a(b(a(a(x1))))) | (8) |
b(a(b(a(a(x1))))) | → | b(a(b(b(a(x1))))) | (9) |
a(b(a(b(b(x1))))) | → | a(b(b(a(a(x1))))) | (10) |
a(a(a(b(b(x1))))) | → | a(a(b(a(a(x1))))) | (11) |
a(a(b(a(a(x1))))) | → | a(a(b(b(a(x1))))) | (12) |
As carrier we take the set {0,1}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 2):
[b(x1)] | = | 2x1 + 0 |
[a(x1)] | = | 2x1 + 1 |
b0(b1(a0(b0(b0(x1))))) | → | b0(b0(b1(a1(a0(x1))))) | (93) |
b0(b1(a0(b0(b1(x1))))) | → | b0(b0(b1(a1(a1(x1))))) | (94) |
a0(b1(a0(b0(b0(x1))))) | → | a0(b0(b1(a1(a0(x1))))) | (95) |
a0(b1(a0(b0(b1(x1))))) | → | a0(b0(b1(a1(a1(x1))))) | (96) |
b1(a1(a0(b0(b0(x1))))) | → | b1(a0(b1(a1(a0(x1))))) | (97) |
b1(a1(a0(b0(b1(x1))))) | → | b1(a0(b1(a1(a1(x1))))) | (98) |
a1(a1(a0(b0(b0(x1))))) | → | a1(a0(b1(a1(a0(x1))))) | (99) |
a1(a1(a0(b0(b1(x1))))) | → | a1(a0(b1(a1(a1(x1))))) | (100) |
b1(a0(b1(a1(a0(x1))))) | → | b1(a0(b0(b1(a0(x1))))) | (101) |
b1(a0(b1(a1(a1(x1))))) | → | b1(a0(b0(b1(a1(x1))))) | (102) |
a1(a0(b1(a1(a0(x1))))) | → | a1(a0(b0(b1(a0(x1))))) | (103) |
a1(a0(b1(a1(a1(x1))))) | → | a1(a0(b0(b1(a1(x1))))) | (104) |
b0(b0(a0(b1(b0(x1))))) | → | a0(a1(b1(b0(b0(x1))))) | (105) |
b1(b0(a0(b1(b0(x1))))) | → | a1(a1(b1(b0(b0(x1))))) | (106) |
b0(b0(a0(b1(a0(x1))))) | → | a0(a1(b1(b0(a0(x1))))) | (107) |
b1(b0(a0(b1(a0(x1))))) | → | a1(a1(b1(b0(a0(x1))))) | (108) |
b0(b0(a0(a1(b1(x1))))) | → | a0(a1(b1(a0(b1(x1))))) | (109) |
b1(b0(a0(a1(b1(x1))))) | → | a1(a1(b1(a0(b1(x1))))) | (110) |
b0(b0(a0(a1(a1(x1))))) | → | a0(a1(b1(a0(a1(x1))))) | (111) |
b1(b0(a0(a1(a1(x1))))) | → | a1(a1(b1(a0(a1(x1))))) | (112) |
a0(a1(b1(a0(b1(x1))))) | → | a0(b1(b0(a0(b1(x1))))) | (113) |
a1(a1(b1(a0(b1(x1))))) | → | a1(b1(b0(a0(b1(x1))))) | (114) |
a0(a1(b1(a0(a1(x1))))) | → | a0(b1(b0(a0(a1(x1))))) | (115) |
a1(a1(b1(a0(a1(x1))))) | → | a1(b1(b0(a0(a1(x1))))) | (116) |
[b0(x1)] | = |
|
||||||||
[b1(x1)] | = |
|
||||||||
[a0(x1)] | = |
|
||||||||
[a1(x1)] | = |
|
b0(b0(a0(b1(b0(x1))))) | → | a0(a1(b1(b0(b0(x1))))) | (105) |
b1(b0(a0(b1(b0(x1))))) | → | a1(a1(b1(b0(b0(x1))))) | (106) |
b0(b0(a0(b1(a0(x1))))) | → | a0(a1(b1(b0(a0(x1))))) | (107) |
b1(b0(a0(b1(a0(x1))))) | → | a1(a1(b1(b0(a0(x1))))) | (108) |
b0(b0(a0(a1(b1(x1))))) | → | a0(a1(b1(a0(b1(x1))))) | (109) |
b1(b0(a0(a1(b1(x1))))) | → | a1(a1(b1(a0(b1(x1))))) | (110) |
b0(b0(a0(a1(a1(x1))))) | → | a0(a1(b1(a0(a1(x1))))) | (111) |
b1(b0(a0(a1(a1(x1))))) | → | a1(a1(b1(a0(a1(x1))))) | (112) |
a0(a1(b1(a0(b1(x1))))) | → | a0(b1(b0(a0(b1(x1))))) | (113) |
a1(a1(b1(a0(b1(x1))))) | → | a1(b1(b0(a0(b1(x1))))) | (114) |
a0(a1(b1(a0(a1(x1))))) | → | a0(b1(b0(a0(a1(x1))))) | (115) |
a1(a1(b1(a0(a1(x1))))) | → | a1(b1(b0(a0(a1(x1))))) | (116) |
There are no rules.
There are no rules in the TRS. Hence, it is terminating.