The rewrite relation of the following TRS is considered.
a(a(x1)) | → | b(x1) | (1) |
a(a(a(x1))) | → | a(b(a(x1))) | (2) |
a(b(a(x1))) | → | b(b(b(x1))) | (3) |
a(a(a(a(x1)))) | → | a(a(b(a(a(x1))))) | (4) |
a(a(b(a(x1)))) | → | a(b(b(a(b(x1))))) | (5) |
a(b(a(a(x1)))) | → | b(a(b(b(a(x1))))) | (6) |
a(b(b(a(x1)))) | → | b(b(b(b(b(x1))))) | (7) |
a(a(a(a(a(x1))))) | → | a(a(a(b(a(a(a(x1))))))) | (8) |
a(a(a(b(a(x1))))) | → | a(a(b(b(a(a(b(x1))))))) | (9) |
a(a(b(a(a(x1))))) | → | a(b(a(b(a(b(a(x1))))))) | (10) |
a(a(b(b(a(x1))))) | → | a(b(b(b(a(b(b(x1))))))) | (11) |
a(b(a(a(a(x1))))) | → | b(a(a(b(b(a(a(x1))))))) | (12) |
a(b(a(b(a(x1))))) | → | b(a(b(b(b(a(b(x1))))))) | (13) |
a(b(b(a(a(x1))))) | → | b(b(a(b(b(b(a(x1))))))) | (14) |
a(b(b(b(a(x1))))) | → | b(b(b(b(b(b(b(x1))))))) | (15) |
{b(☐), a(☐)}
We obtain the transformed TRSb(a(a(x1))) | → | b(b(x1)) | (16) |
b(a(a(a(x1)))) | → | b(a(b(a(x1)))) | (17) |
b(a(b(a(x1)))) | → | b(b(b(b(x1)))) | (18) |
b(a(a(a(a(x1))))) | → | b(a(a(b(a(a(x1)))))) | (19) |
b(a(a(b(a(x1))))) | → | b(a(b(b(a(b(x1)))))) | (20) |
b(a(b(a(a(x1))))) | → | b(b(a(b(b(a(x1)))))) | (21) |
b(a(b(b(a(x1))))) | → | b(b(b(b(b(b(x1)))))) | (22) |
b(a(a(a(a(a(x1)))))) | → | b(a(a(a(b(a(a(a(x1)))))))) | (23) |
b(a(a(a(b(a(x1)))))) | → | b(a(a(b(b(a(a(b(x1)))))))) | (24) |
b(a(a(b(a(a(x1)))))) | → | b(a(b(a(b(a(b(a(x1)))))))) | (25) |
b(a(a(b(b(a(x1)))))) | → | b(a(b(b(b(a(b(b(x1)))))))) | (26) |
b(a(b(a(a(a(x1)))))) | → | b(b(a(a(b(b(a(a(x1)))))))) | (27) |
b(a(b(a(b(a(x1)))))) | → | b(b(a(b(b(b(a(b(x1)))))))) | (28) |
b(a(b(b(a(a(x1)))))) | → | b(b(b(a(b(b(b(a(x1)))))))) | (29) |
b(a(b(b(b(a(x1)))))) | → | b(b(b(b(b(b(b(b(x1)))))))) | (30) |
a(a(a(x1))) | → | a(b(x1)) | (31) |
a(a(a(a(x1)))) | → | a(a(b(a(x1)))) | (32) |
a(a(b(a(x1)))) | → | a(b(b(b(x1)))) | (33) |
a(a(a(a(a(x1))))) | → | a(a(a(b(a(a(x1)))))) | (34) |
a(a(a(b(a(x1))))) | → | a(a(b(b(a(b(x1)))))) | (35) |
a(a(b(a(a(x1))))) | → | a(b(a(b(b(a(x1)))))) | (36) |
a(a(b(b(a(x1))))) | → | a(b(b(b(b(b(x1)))))) | (37) |
a(a(a(a(a(a(x1)))))) | → | a(a(a(a(b(a(a(a(x1)))))))) | (38) |
a(a(a(a(b(a(x1)))))) | → | a(a(a(b(b(a(a(b(x1)))))))) | (39) |
a(a(a(b(a(a(x1)))))) | → | a(a(b(a(b(a(b(a(x1)))))))) | (40) |
a(a(a(b(b(a(x1)))))) | → | a(a(b(b(b(a(b(b(x1)))))))) | (41) |
a(a(b(a(a(a(x1)))))) | → | a(b(a(a(b(b(a(a(x1)))))))) | (42) |
a(a(b(a(b(a(x1)))))) | → | a(b(a(b(b(b(a(b(x1)))))))) | (43) |
a(a(b(b(a(a(x1)))))) | → | a(b(b(a(b(b(b(a(x1)))))))) | (44) |
a(a(b(b(b(a(x1)))))) | → | a(b(b(b(b(b(b(b(x1)))))))) | (45) |
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 |
a1(a1(a1(x1))) | → | a0(b1(x1)) | (46) |
a1(a1(a0(x1))) | → | a0(b0(x1)) | (47) |
b1(a1(a1(x1))) | → | b0(b1(x1)) | (48) |
b1(a1(a0(x1))) | → | b0(b0(x1)) | (49) |
a1(a1(a1(a1(x1)))) | → | a1(a0(b1(a1(x1)))) | (50) |
a1(a1(a1(a0(x1)))) | → | a1(a0(b1(a0(x1)))) | (51) |
b1(a1(a1(a1(x1)))) | → | b1(a0(b1(a1(x1)))) | (52) |
b1(a1(a1(a0(x1)))) | → | b1(a0(b1(a0(x1)))) | (53) |
a1(a0(b1(a1(x1)))) | → | a0(b0(b0(b1(x1)))) | (54) |
a1(a0(b1(a0(x1)))) | → | a0(b0(b0(b0(x1)))) | (55) |
b1(a0(b1(a1(x1)))) | → | b0(b0(b0(b1(x1)))) | (56) |
b1(a0(b1(a0(x1)))) | → | b0(b0(b0(b0(x1)))) | (57) |
a1(a1(a1(a1(a1(x1))))) | → | a1(a1(a0(b1(a1(a1(x1)))))) | (58) |
a1(a1(a1(a1(a0(x1))))) | → | a1(a1(a0(b1(a1(a0(x1)))))) | (59) |
b1(a1(a1(a1(a1(x1))))) | → | b1(a1(a0(b1(a1(a1(x1)))))) | (60) |
b1(a1(a1(a1(a0(x1))))) | → | b1(a1(a0(b1(a1(a0(x1)))))) | (61) |
a1(a1(a0(b1(a1(x1))))) | → | a1(a0(b0(b1(a0(b1(x1)))))) | (62) |
a1(a1(a0(b1(a0(x1))))) | → | a1(a0(b0(b1(a0(b0(x1)))))) | (63) |
b1(a1(a0(b1(a1(x1))))) | → | b1(a0(b0(b1(a0(b1(x1)))))) | (64) |
b1(a1(a0(b1(a0(x1))))) | → | b1(a0(b0(b1(a0(b0(x1)))))) | (65) |
a1(a0(b1(a1(a1(x1))))) | → | a0(b1(a0(b0(b1(a1(x1)))))) | (66) |
a1(a0(b1(a1(a0(x1))))) | → | a0(b1(a0(b0(b1(a0(x1)))))) | (67) |
b1(a0(b1(a1(a1(x1))))) | → | b0(b1(a0(b0(b1(a1(x1)))))) | (68) |
b1(a0(b1(a1(a0(x1))))) | → | b0(b1(a0(b0(b1(a0(x1)))))) | (69) |
a1(a0(b0(b1(a1(x1))))) | → | a0(b0(b0(b0(b0(b1(x1)))))) | (70) |
a1(a0(b0(b1(a0(x1))))) | → | a0(b0(b0(b0(b0(b0(x1)))))) | (71) |
b1(a0(b0(b1(a1(x1))))) | → | b0(b0(b0(b0(b0(b1(x1)))))) | (72) |
b1(a0(b0(b1(a0(x1))))) | → | b0(b0(b0(b0(b0(b0(x1)))))) | (73) |
a1(a1(a1(a1(a1(a1(x1)))))) | → | a1(a1(a1(a0(b1(a1(a1(a1(x1)))))))) | (74) |
a1(a1(a1(a1(a1(a0(x1)))))) | → | a1(a1(a1(a0(b1(a1(a1(a0(x1)))))))) | (75) |
b1(a1(a1(a1(a1(a1(x1)))))) | → | b1(a1(a1(a0(b1(a1(a1(a1(x1)))))))) | (76) |
b1(a1(a1(a1(a1(a0(x1)))))) | → | b1(a1(a1(a0(b1(a1(a1(a0(x1)))))))) | (77) |
a1(a1(a1(a0(b1(a1(x1)))))) | → | a1(a1(a0(b0(b1(a1(a0(b1(x1)))))))) | (78) |
a1(a1(a1(a0(b1(a0(x1)))))) | → | a1(a1(a0(b0(b1(a1(a0(b0(x1)))))))) | (79) |
b1(a1(a1(a0(b1(a1(x1)))))) | → | b1(a1(a0(b0(b1(a1(a0(b1(x1)))))))) | (80) |
b1(a1(a1(a0(b1(a0(x1)))))) | → | b1(a1(a0(b0(b1(a1(a0(b0(x1)))))))) | (81) |
a1(a1(a0(b1(a1(a1(x1)))))) | → | a1(a0(b1(a0(b1(a0(b1(a1(x1)))))))) | (82) |
a1(a1(a0(b1(a1(a0(x1)))))) | → | a1(a0(b1(a0(b1(a0(b1(a0(x1)))))))) | (83) |
b1(a1(a0(b1(a1(a1(x1)))))) | → | b1(a0(b1(a0(b1(a0(b1(a1(x1)))))))) | (84) |
b1(a1(a0(b1(a1(a0(x1)))))) | → | b1(a0(b1(a0(b1(a0(b1(a0(x1)))))))) | (85) |
a1(a1(a0(b0(b1(a1(x1)))))) | → | a1(a0(b0(b0(b1(a0(b0(b1(x1)))))))) | (86) |
a1(a1(a0(b0(b1(a0(x1)))))) | → | a1(a0(b0(b0(b1(a0(b0(b0(x1)))))))) | (87) |
b1(a1(a0(b0(b1(a1(x1)))))) | → | b1(a0(b0(b0(b1(a0(b0(b1(x1)))))))) | (88) |
b1(a1(a0(b0(b1(a0(x1)))))) | → | b1(a0(b0(b0(b1(a0(b0(b0(x1)))))))) | (89) |
a1(a0(b1(a1(a1(a1(x1)))))) | → | a0(b1(a1(a0(b0(b1(a1(a1(x1)))))))) | (90) |
a1(a0(b1(a1(a1(a0(x1)))))) | → | a0(b1(a1(a0(b0(b1(a1(a0(x1)))))))) | (91) |
b1(a0(b1(a1(a1(a1(x1)))))) | → | b0(b1(a1(a0(b0(b1(a1(a1(x1)))))))) | (92) |
b1(a0(b1(a1(a1(a0(x1)))))) | → | b0(b1(a1(a0(b0(b1(a1(a0(x1)))))))) | (93) |
a1(a0(b1(a0(b1(a1(x1)))))) | → | a0(b1(a0(b0(b0(b1(a0(b1(x1)))))))) | (94) |
a1(a0(b1(a0(b1(a0(x1)))))) | → | a0(b1(a0(b0(b0(b1(a0(b0(x1)))))))) | (95) |
b1(a0(b1(a0(b1(a1(x1)))))) | → | b0(b1(a0(b0(b0(b1(a0(b1(x1)))))))) | (96) |
b1(a0(b1(a0(b1(a0(x1)))))) | → | b0(b1(a0(b0(b0(b1(a0(b0(x1)))))))) | (97) |
a1(a0(b0(b1(a1(a1(x1)))))) | → | a0(b0(b1(a0(b0(b0(b1(a1(x1)))))))) | (98) |
a1(a0(b0(b1(a1(a0(x1)))))) | → | a0(b0(b1(a0(b0(b0(b1(a0(x1)))))))) | (99) |
b1(a0(b0(b1(a1(a1(x1)))))) | → | b0(b0(b1(a0(b0(b0(b1(a1(x1)))))))) | (100) |
b1(a0(b0(b1(a1(a0(x1)))))) | → | b0(b0(b1(a0(b0(b0(b1(a0(x1)))))))) | (101) |
a1(a0(b0(b0(b1(a1(x1)))))) | → | a0(b0(b0(b0(b0(b0(b0(b1(x1)))))))) | (102) |
a1(a0(b0(b0(b1(a0(x1)))))) | → | a0(b0(b0(b0(b0(b0(b0(b0(x1)))))))) | (103) |
b1(a0(b0(b0(b1(a1(x1)))))) | → | b0(b0(b0(b0(b0(b0(b0(b1(x1)))))))) | (104) |
b1(a0(b0(b0(b1(a0(x1)))))) | → | b0(b0(b0(b0(b0(b0(b0(b0(x1)))))))) | (105) |
[b0(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[a0(x1)] | = |
x1 +
|
||||
[a1(x1)] | = |
x1 +
|
a1(a1(a1(x1))) | → | a0(b1(x1)) | (46) |
a1(a1(a0(x1))) | → | a0(b0(x1)) | (47) |
b1(a1(a1(x1))) | → | b0(b1(x1)) | (48) |
b1(a1(a0(x1))) | → | b0(b0(x1)) | (49) |
a1(a1(a1(a1(x1)))) | → | a1(a0(b1(a1(x1)))) | (50) |
a1(a1(a1(a0(x1)))) | → | a1(a0(b1(a0(x1)))) | (51) |
b1(a1(a1(a1(x1)))) | → | b1(a0(b1(a1(x1)))) | (52) |
b1(a1(a1(a0(x1)))) | → | b1(a0(b1(a0(x1)))) | (53) |
a1(a0(b1(a1(x1)))) | → | a0(b0(b0(b1(x1)))) | (54) |
a1(a0(b1(a0(x1)))) | → | a0(b0(b0(b0(x1)))) | (55) |
b1(a0(b1(a1(x1)))) | → | b0(b0(b0(b1(x1)))) | (56) |
a1(a1(a1(a1(a1(x1))))) | → | a1(a1(a0(b1(a1(a1(x1)))))) | (58) |
a1(a1(a1(a1(a0(x1))))) | → | a1(a1(a0(b1(a1(a0(x1)))))) | (59) |
b1(a1(a1(a1(a1(x1))))) | → | b1(a1(a0(b1(a1(a1(x1)))))) | (60) |
b1(a1(a1(a1(a0(x1))))) | → | b1(a1(a0(b1(a1(a0(x1)))))) | (61) |
a1(a1(a0(b1(a1(x1))))) | → | a1(a0(b0(b1(a0(b1(x1)))))) | (62) |
a1(a1(a0(b1(a0(x1))))) | → | a1(a0(b0(b1(a0(b0(x1)))))) | (63) |
b1(a1(a0(b1(a1(x1))))) | → | b1(a0(b0(b1(a0(b1(x1)))))) | (64) |
b1(a1(a0(b1(a0(x1))))) | → | b1(a0(b0(b1(a0(b0(x1)))))) | (65) |
a1(a0(b1(a1(a1(x1))))) | → | a0(b1(a0(b0(b1(a1(x1)))))) | (66) |
a1(a0(b1(a1(a0(x1))))) | → | a0(b1(a0(b0(b1(a0(x1)))))) | (67) |
b1(a0(b1(a1(a1(x1))))) | → | b0(b1(a0(b0(b1(a1(x1)))))) | (68) |
b1(a0(b1(a1(a0(x1))))) | → | b0(b1(a0(b0(b1(a0(x1)))))) | (69) |
a1(a0(b0(b1(a1(x1))))) | → | a0(b0(b0(b0(b0(b1(x1)))))) | (70) |
a1(a0(b0(b1(a0(x1))))) | → | a0(b0(b0(b0(b0(b0(x1)))))) | (71) |
b1(a0(b0(b1(a1(x1))))) | → | b0(b0(b0(b0(b0(b1(x1)))))) | (72) |
a1(a1(a1(a0(b1(a1(x1)))))) | → | a1(a1(a0(b0(b1(a1(a0(b1(x1)))))))) | (78) |
b1(a1(a1(a0(b1(a1(x1)))))) | → | b1(a1(a0(b0(b1(a1(a0(b1(x1)))))))) | (80) |
a1(a1(a0(b1(a1(a1(x1)))))) | → | a1(a0(b1(a0(b1(a0(b1(a1(x1)))))))) | (82) |
a1(a1(a0(b1(a1(a0(x1)))))) | → | a1(a0(b1(a0(b1(a0(b1(a0(x1)))))))) | (83) |
b1(a1(a0(b1(a1(a1(x1)))))) | → | b1(a0(b1(a0(b1(a0(b1(a1(x1)))))))) | (84) |
b1(a1(a0(b1(a1(a0(x1)))))) | → | b1(a0(b1(a0(b1(a0(b1(a0(x1)))))))) | (85) |
a1(a1(a0(b0(b1(a1(x1)))))) | → | a1(a0(b0(b0(b1(a0(b0(b1(x1)))))))) | (86) |
a1(a1(a0(b0(b1(a0(x1)))))) | → | a1(a0(b0(b0(b1(a0(b0(b0(x1)))))))) | (87) |
b1(a1(a0(b0(b1(a1(x1)))))) | → | b1(a0(b0(b0(b1(a0(b0(b1(x1)))))))) | (88) |
b1(a1(a0(b0(b1(a0(x1)))))) | → | b1(a0(b0(b0(b1(a0(b0(b0(x1)))))))) | (89) |
a1(a0(b1(a1(a1(a1(x1)))))) | → | a0(b1(a1(a0(b0(b1(a1(a1(x1)))))))) | (90) |
a1(a0(b1(a1(a1(a0(x1)))))) | → | a0(b1(a1(a0(b0(b1(a1(a0(x1)))))))) | (91) |
a1(a0(b1(a0(b1(a1(x1)))))) | → | a0(b1(a0(b0(b0(b1(a0(b1(x1)))))))) | (94) |
a1(a0(b1(a0(b1(a0(x1)))))) | → | a0(b1(a0(b0(b0(b1(a0(b0(x1)))))))) | (95) |
b1(a0(b1(a0(b1(a1(x1)))))) | → | b0(b1(a0(b0(b0(b1(a0(b1(x1)))))))) | (96) |
a1(a0(b0(b1(a1(a1(x1)))))) | → | a0(b0(b1(a0(b0(b0(b1(a1(x1)))))))) | (98) |
a1(a0(b0(b1(a1(a0(x1)))))) | → | a0(b0(b1(a0(b0(b0(b1(a0(x1)))))))) | (99) |
b1(a0(b0(b1(a1(a1(x1)))))) | → | b0(b0(b1(a0(b0(b0(b1(a1(x1)))))))) | (100) |
b1(a0(b0(b1(a1(a0(x1)))))) | → | b0(b0(b1(a0(b0(b0(b1(a0(x1)))))))) | (101) |
a1(a0(b0(b0(b1(a1(x1)))))) | → | a0(b0(b0(b0(b0(b0(b0(b1(x1)))))))) | (102) |
a1(a0(b0(b0(b1(a0(x1)))))) | → | a0(b0(b0(b0(b0(b0(b0(b0(x1)))))))) | (103) |
b1(a0(b0(b0(b1(a1(x1)))))) | → | b0(b0(b0(b0(b0(b0(b0(b1(x1)))))))) | (104) |
a0(b1(a0(b1(x1)))) | → | b0(b0(b0(b0(x1)))) | (106) |
a0(b1(b0(a0(b1(x1))))) | → | b0(b0(b0(b0(b0(b0(x1)))))) | (107) |
a1(a1(a1(a1(a1(a1(x1)))))) | → | a1(a1(a1(b1(a0(a1(a1(a1(x1)))))))) | (108) |
a0(a1(a1(a1(a1(a1(x1)))))) | → | a0(a1(a1(b1(a0(a1(a1(a1(x1)))))))) | (109) |
a1(a1(a1(a1(a1(b1(x1)))))) | → | a1(a1(a1(b1(a0(a1(a1(b1(x1)))))))) | (110) |
a0(a1(a1(a1(a1(b1(x1)))))) | → | a0(a1(a1(b1(a0(a1(a1(b1(x1)))))))) | (111) |
a0(b1(a0(a1(a1(a1(x1)))))) | → | b0(a0(a1(b1(b0(a0(a1(a1(x1)))))))) | (112) |
a0(b1(a0(a1(a1(b1(x1)))))) | → | b0(a0(a1(b1(b0(a0(a1(b1(x1)))))))) | (113) |
a1(a1(a1(b1(a0(b1(x1)))))) | → | a1(a1(b1(b0(a0(a1(b1(b0(x1)))))))) | (114) |
a0(a1(a1(b1(a0(b1(x1)))))) | → | a0(a1(b1(b0(a0(a1(b1(b0(x1)))))))) | (115) |
a0(b1(a0(b1(a0(b1(x1)))))) | → | b0(a0(b1(b0(b0(a0(b1(b0(x1)))))))) | (116) |
a0(b1(b0(b0(a0(b1(x1)))))) | → | b0(b0(b0(b0(b0(b0(b0(b0(x1)))))))) | (117) |
a0#(b1(a0(b1(a0(b1(x1)))))) | → | a0#(b1(b0(x1))) | (118) |
a0#(b1(a0(b1(a0(b1(x1)))))) | → | a0#(b1(b0(b0(a0(b1(b0(x1))))))) | (119) |
a0#(b1(a0(a1(a1(b1(x1)))))) | → | a0#(a1(b1(x1))) | (120) |
a0#(b1(a0(a1(a1(b1(x1)))))) | → | a0#(a1(b1(b0(a0(a1(b1(x1))))))) | (121) |
a0#(b1(a0(a1(a1(b1(x1)))))) | → | a1#(b1(b0(a0(a1(b1(x1)))))) | (122) |
a0#(b1(a0(a1(a1(a1(x1)))))) | → | a0#(a1(b1(b0(a0(a1(a1(x1))))))) | (123) |
a0#(b1(a0(a1(a1(a1(x1)))))) | → | a0#(a1(a1(x1))) | (124) |
a0#(b1(a0(a1(a1(a1(x1)))))) | → | a1#(b1(b0(a0(a1(a1(x1)))))) | (125) |
a0#(a1(a1(b1(a0(b1(x1)))))) | → | a0#(a1(b1(b0(x1)))) | (126) |
a0#(a1(a1(b1(a0(b1(x1)))))) | → | a0#(a1(b1(b0(a0(a1(b1(b0(x1)))))))) | (127) |
a0#(a1(a1(b1(a0(b1(x1)))))) | → | a1#(b1(b0(x1))) | (128) |
a0#(a1(a1(b1(a0(b1(x1)))))) | → | a1#(b1(b0(a0(a1(b1(b0(x1))))))) | (129) |
a0#(a1(a1(a1(a1(b1(x1)))))) | → | a0#(a1(a1(b1(x1)))) | (130) |
a0#(a1(a1(a1(a1(b1(x1)))))) | → | a0#(a1(a1(b1(a0(a1(a1(b1(x1)))))))) | (131) |
a0#(a1(a1(a1(a1(b1(x1)))))) | → | a1#(b1(a0(a1(a1(b1(x1)))))) | (132) |
a0#(a1(a1(a1(a1(b1(x1)))))) | → | a1#(a1(b1(a0(a1(a1(b1(x1))))))) | (133) |
a0#(a1(a1(a1(a1(a1(x1)))))) | → | a0#(a1(a1(b1(a0(a1(a1(a1(x1)))))))) | (134) |
a0#(a1(a1(a1(a1(a1(x1)))))) | → | a0#(a1(a1(a1(x1)))) | (135) |
a0#(a1(a1(a1(a1(a1(x1)))))) | → | a1#(b1(a0(a1(a1(a1(x1)))))) | (136) |
a0#(a1(a1(a1(a1(a1(x1)))))) | → | a1#(a1(b1(a0(a1(a1(a1(x1))))))) | (137) |
a1#(a1(a1(b1(a0(b1(x1)))))) | → | a0#(a1(b1(b0(x1)))) | (138) |
a1#(a1(a1(b1(a0(b1(x1)))))) | → | a1#(b1(b0(x1))) | (139) |
a1#(a1(a1(b1(a0(b1(x1)))))) | → | a1#(b1(b0(a0(a1(b1(b0(x1))))))) | (140) |
a1#(a1(a1(b1(a0(b1(x1)))))) | → | a1#(a1(b1(b0(a0(a1(b1(b0(x1)))))))) | (141) |
a1#(a1(a1(a1(a1(b1(x1)))))) | → | a0#(a1(a1(b1(x1)))) | (142) |
a1#(a1(a1(a1(a1(b1(x1)))))) | → | a1#(b1(a0(a1(a1(b1(x1)))))) | (143) |
a1#(a1(a1(a1(a1(b1(x1)))))) | → | a1#(a1(b1(a0(a1(a1(b1(x1))))))) | (144) |
a1#(a1(a1(a1(a1(b1(x1)))))) | → | a1#(a1(a1(b1(a0(a1(a1(b1(x1)))))))) | (145) |
a1#(a1(a1(a1(a1(a1(x1)))))) | → | a0#(a1(a1(a1(x1)))) | (146) |
a1#(a1(a1(a1(a1(a1(x1)))))) | → | a1#(b1(a0(a1(a1(a1(x1)))))) | (147) |
a1#(a1(a1(a1(a1(a1(x1)))))) | → | a1#(a1(b1(a0(a1(a1(a1(x1))))))) | (148) |
a1#(a1(a1(a1(a1(a1(x1)))))) | → | a1#(a1(a1(b1(a0(a1(a1(a1(x1)))))))) | (149) |
[b0(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[a0(x1)] | = |
x1 +
|
||||
[a1(x1)] | = |
x1 +
|
||||
[a0#(x1)] | = |
x1 +
|
||||
[a1#(x1)] | = |
x1 +
|
a0(b1(a0(b1(x1)))) | → | b0(b0(b0(b0(x1)))) | (106) |
a0(b1(b0(a0(b1(x1))))) | → | b0(b0(b0(b0(b0(b0(x1)))))) | (107) |
a1(a1(a1(a1(a1(a1(x1)))))) | → | a1(a1(a1(b1(a0(a1(a1(a1(x1)))))))) | (108) |
a0(a1(a1(a1(a1(a1(x1)))))) | → | a0(a1(a1(b1(a0(a1(a1(a1(x1)))))))) | (109) |
a1(a1(a1(a1(a1(b1(x1)))))) | → | a1(a1(a1(b1(a0(a1(a1(b1(x1)))))))) | (110) |
a0(a1(a1(a1(a1(b1(x1)))))) | → | a0(a1(a1(b1(a0(a1(a1(b1(x1)))))))) | (111) |
a0(b1(a0(a1(a1(a1(x1)))))) | → | b0(a0(a1(b1(b0(a0(a1(a1(x1)))))))) | (112) |
a0(b1(a0(a1(a1(b1(x1)))))) | → | b0(a0(a1(b1(b0(a0(a1(b1(x1)))))))) | (113) |
a1(a1(a1(b1(a0(b1(x1)))))) | → | a1(a1(b1(b0(a0(a1(b1(b0(x1)))))))) | (114) |
a0(a1(a1(b1(a0(b1(x1)))))) | → | a0(a1(b1(b0(a0(a1(b1(b0(x1)))))))) | (115) |
a0(b1(a0(b1(a0(b1(x1)))))) | → | b0(a0(b1(b0(b0(a0(b1(b0(x1)))))))) | (116) |
a0(b1(b0(b0(a0(b1(x1)))))) | → | b0(b0(b0(b0(b0(b0(b0(b0(x1)))))))) | (117) |
a0#(b1(a0(a1(a1(b1(x1)))))) | → | a0#(a1(b1(x1))) | (120) |
a0#(b1(a0(a1(a1(b1(x1)))))) | → | a1#(b1(b0(a0(a1(b1(x1)))))) | (122) |
a0#(b1(a0(a1(a1(a1(x1)))))) | → | a0#(a1(a1(x1))) | (124) |
a0#(b1(a0(a1(a1(a1(x1)))))) | → | a1#(b1(b0(a0(a1(a1(x1)))))) | (125) |
a0#(a1(a1(b1(a0(b1(x1)))))) | → | a0#(a1(b1(b0(x1)))) | (126) |
a0#(a1(a1(b1(a0(b1(x1)))))) | → | a1#(b1(b0(x1))) | (128) |
a0#(a1(a1(b1(a0(b1(x1)))))) | → | a1#(b1(b0(a0(a1(b1(b0(x1))))))) | (129) |
a0#(a1(a1(a1(a1(b1(x1)))))) | → | a0#(a1(a1(b1(x1)))) | (130) |
a0#(a1(a1(a1(a1(b1(x1)))))) | → | a1#(b1(a0(a1(a1(b1(x1)))))) | (132) |
a0#(a1(a1(a1(a1(b1(x1)))))) | → | a1#(a1(b1(a0(a1(a1(b1(x1))))))) | (133) |
a0#(a1(a1(a1(a1(a1(x1)))))) | → | a0#(a1(a1(a1(x1)))) | (135) |
a0#(a1(a1(a1(a1(a1(x1)))))) | → | a1#(b1(a0(a1(a1(a1(x1)))))) | (136) |
a0#(a1(a1(a1(a1(a1(x1)))))) | → | a1#(a1(b1(a0(a1(a1(a1(x1))))))) | (137) |
a1#(a1(a1(b1(a0(b1(x1)))))) | → | a0#(a1(b1(b0(x1)))) | (138) |
a1#(a1(a1(b1(a0(b1(x1)))))) | → | a1#(b1(b0(x1))) | (139) |
a1#(a1(a1(b1(a0(b1(x1)))))) | → | a1#(b1(b0(a0(a1(b1(b0(x1))))))) | (140) |
a1#(a1(a1(a1(a1(b1(x1)))))) | → | a0#(a1(a1(b1(x1)))) | (142) |
a1#(a1(a1(a1(a1(b1(x1)))))) | → | a1#(b1(a0(a1(a1(b1(x1)))))) | (143) |
a1#(a1(a1(a1(a1(b1(x1)))))) | → | a1#(a1(b1(a0(a1(a1(b1(x1))))))) | (144) |
a1#(a1(a1(a1(a1(a1(x1)))))) | → | a0#(a1(a1(a1(x1)))) | (146) |
a1#(a1(a1(a1(a1(a1(x1)))))) | → | a1#(b1(a0(a1(a1(a1(x1)))))) | (147) |
a1#(a1(a1(a1(a1(a1(x1)))))) | → | a1#(a1(b1(a0(a1(a1(a1(x1))))))) | (148) |
The dependency pairs are split into 0 components.