The rewrite relation of the following TRS is considered.
a(x1) | → | x1 | (1) |
a(a(x1)) | → | b(x1) | (2) |
b(x1) | → | x1 | (3) |
b(c(x1)) | → | c(c(c(b(a(x1))))) | (4) |
a(x1) | → | x1 | (1) |
a(a(x1)) | → | b(x1) | (2) |
b(x1) | → | x1 | (3) |
c(b(x1)) | → | a(b(c(c(c(x1))))) | (5) |
{a(☐), b(☐), c(☐)}
We obtain the transformed TRSa(a(x1)) | → | a(x1) | (6) |
b(a(x1)) | → | b(x1) | (7) |
c(a(x1)) | → | c(x1) | (8) |
a(a(a(x1))) | → | a(b(x1)) | (9) |
b(a(a(x1))) | → | b(b(x1)) | (10) |
c(a(a(x1))) | → | c(b(x1)) | (11) |
a(b(x1)) | → | a(x1) | (12) |
b(b(x1)) | → | b(x1) | (13) |
c(b(x1)) | → | c(x1) | (14) |
a(c(b(x1))) | → | a(a(b(c(c(c(x1)))))) | (15) |
b(c(b(x1))) | → | b(a(b(c(c(c(x1)))))) | (16) |
c(c(b(x1))) | → | c(a(b(c(c(c(x1)))))) | (17) |
Root-labeling is applied.
We obtain the labeled TRSaa(aa(x1)) | → | aa(x1) | (18) |
aa(ab(x1)) | → | ab(x1) | (19) |
aa(ac(x1)) | → | ac(x1) | (20) |
ba(aa(x1)) | → | ba(x1) | (21) |
ba(ab(x1)) | → | bb(x1) | (22) |
ba(ac(x1)) | → | bc(x1) | (23) |
ca(aa(x1)) | → | ca(x1) | (24) |
ca(ab(x1)) | → | cb(x1) | (25) |
ca(ac(x1)) | → | cc(x1) | (26) |
aa(aa(aa(x1))) | → | ab(ba(x1)) | (27) |
aa(aa(ab(x1))) | → | ab(bb(x1)) | (28) |
aa(aa(ac(x1))) | → | ab(bc(x1)) | (29) |
ba(aa(aa(x1))) | → | bb(ba(x1)) | (30) |
ba(aa(ab(x1))) | → | bb(bb(x1)) | (31) |
ba(aa(ac(x1))) | → | bb(bc(x1)) | (32) |
ca(aa(aa(x1))) | → | cb(ba(x1)) | (33) |
ca(aa(ab(x1))) | → | cb(bb(x1)) | (34) |
ca(aa(ac(x1))) | → | cb(bc(x1)) | (35) |
ab(ba(x1)) | → | aa(x1) | (36) |
ab(bb(x1)) | → | ab(x1) | (37) |
ab(bc(x1)) | → | ac(x1) | (38) |
bb(ba(x1)) | → | ba(x1) | (39) |
bb(bb(x1)) | → | bb(x1) | (40) |
bb(bc(x1)) | → | bc(x1) | (41) |
cb(ba(x1)) | → | ca(x1) | (42) |
cb(bb(x1)) | → | cb(x1) | (43) |
cb(bc(x1)) | → | cc(x1) | (44) |
ac(cb(ba(x1))) | → | aa(ab(bc(cc(cc(ca(x1)))))) | (45) |
ac(cb(bb(x1))) | → | aa(ab(bc(cc(cc(cb(x1)))))) | (46) |
ac(cb(bc(x1))) | → | aa(ab(bc(cc(cc(cc(x1)))))) | (47) |
bc(cb(ba(x1))) | → | ba(ab(bc(cc(cc(ca(x1)))))) | (48) |
bc(cb(bb(x1))) | → | ba(ab(bc(cc(cc(cb(x1)))))) | (49) |
bc(cb(bc(x1))) | → | ba(ab(bc(cc(cc(cc(x1)))))) | (50) |
cc(cb(ba(x1))) | → | ca(ab(bc(cc(cc(ca(x1)))))) | (51) |
cc(cb(bb(x1))) | → | ca(ab(bc(cc(cc(cb(x1)))))) | (52) |
cc(cb(bc(x1))) | → | ca(ab(bc(cc(cc(cc(x1)))))) | (53) |
[aa(x1)] | = | 1 · x1 + 1 |
[ab(x1)] | = | 1 · x1 |
[ac(x1)] | = | 1 · x1 + 1 |
[ba(x1)] | = | 1 · x1 + 1 |
[bb(x1)] | = | 1 · x1 + 1 |
[bc(x1)] | = | 1 · x1 + 1 |
[ca(x1)] | = | 1 · x1 |
[cb(x1)] | = | 1 · x1 |
[cc(x1)] | = | 1 · x1 |
aa(aa(x1)) | → | aa(x1) | (18) |
aa(ab(x1)) | → | ab(x1) | (19) |
aa(ac(x1)) | → | ac(x1) | (20) |
ba(aa(x1)) | → | ba(x1) | (21) |
ba(ac(x1)) | → | bc(x1) | (23) |
ca(aa(x1)) | → | ca(x1) | (24) |
ca(ac(x1)) | → | cc(x1) | (26) |
aa(aa(aa(x1))) | → | ab(ba(x1)) | (27) |
aa(aa(ab(x1))) | → | ab(bb(x1)) | (28) |
aa(aa(ac(x1))) | → | ab(bc(x1)) | (29) |
ba(aa(aa(x1))) | → | bb(ba(x1)) | (30) |
ba(aa(ac(x1))) | → | bb(bc(x1)) | (32) |
ca(aa(aa(x1))) | → | cb(ba(x1)) | (33) |
ca(aa(ac(x1))) | → | cb(bc(x1)) | (35) |
ab(bb(x1)) | → | ab(x1) | (37) |
bb(ba(x1)) | → | ba(x1) | (39) |
bb(bb(x1)) | → | bb(x1) | (40) |
bb(bc(x1)) | → | bc(x1) | (41) |
cb(ba(x1)) | → | ca(x1) | (42) |
cb(bb(x1)) | → | cb(x1) | (43) |
cb(bc(x1)) | → | cc(x1) | (44) |
ab#(bc(x1)) | → | ac#(x1) | (54) |
ac#(cb(ba(x1))) | → | ab#(bc(cc(cc(ca(x1))))) | (55) |
ac#(cb(ba(x1))) | → | bc#(cc(cc(ca(x1)))) | (56) |
ac#(cb(ba(x1))) | → | cc#(cc(ca(x1))) | (57) |
ac#(cb(ba(x1))) | → | cc#(ca(x1)) | (58) |
ac#(cb(ba(x1))) | → | ca#(x1) | (59) |
ac#(cb(bb(x1))) | → | ab#(bc(cc(cc(cb(x1))))) | (60) |
ac#(cb(bb(x1))) | → | bc#(cc(cc(cb(x1)))) | (61) |
ac#(cb(bb(x1))) | → | cc#(cc(cb(x1))) | (62) |
ac#(cb(bb(x1))) | → | cc#(cb(x1)) | (63) |
ac#(cb(bc(x1))) | → | ab#(bc(cc(cc(cc(x1))))) | (64) |
ac#(cb(bc(x1))) | → | bc#(cc(cc(cc(x1)))) | (65) |
ac#(cb(bc(x1))) | → | cc#(cc(cc(x1))) | (66) |
ac#(cb(bc(x1))) | → | cc#(cc(x1)) | (67) |
ac#(cb(bc(x1))) | → | cc#(x1) | (68) |
bc#(cb(ba(x1))) | → | ba#(ab(bc(cc(cc(ca(x1)))))) | (69) |
bc#(cb(ba(x1))) | → | ab#(bc(cc(cc(ca(x1))))) | (70) |
bc#(cb(ba(x1))) | → | bc#(cc(cc(ca(x1)))) | (71) |
bc#(cb(ba(x1))) | → | cc#(cc(ca(x1))) | (72) |
bc#(cb(ba(x1))) | → | cc#(ca(x1)) | (73) |
bc#(cb(ba(x1))) | → | ca#(x1) | (74) |
bc#(cb(bb(x1))) | → | ba#(ab(bc(cc(cc(cb(x1)))))) | (75) |
bc#(cb(bb(x1))) | → | ab#(bc(cc(cc(cb(x1))))) | (76) |
bc#(cb(bb(x1))) | → | bc#(cc(cc(cb(x1)))) | (77) |
bc#(cb(bb(x1))) | → | cc#(cc(cb(x1))) | (78) |
bc#(cb(bb(x1))) | → | cc#(cb(x1)) | (79) |
bc#(cb(bc(x1))) | → | ba#(ab(bc(cc(cc(cc(x1)))))) | (80) |
bc#(cb(bc(x1))) | → | ab#(bc(cc(cc(cc(x1))))) | (81) |
bc#(cb(bc(x1))) | → | bc#(cc(cc(cc(x1)))) | (82) |
bc#(cb(bc(x1))) | → | cc#(cc(cc(x1))) | (83) |
bc#(cb(bc(x1))) | → | cc#(cc(x1)) | (84) |
bc#(cb(bc(x1))) | → | cc#(x1) | (85) |
cc#(cb(ba(x1))) | → | ca#(ab(bc(cc(cc(ca(x1)))))) | (86) |
cc#(cb(ba(x1))) | → | ab#(bc(cc(cc(ca(x1))))) | (87) |
cc#(cb(ba(x1))) | → | bc#(cc(cc(ca(x1)))) | (88) |
cc#(cb(ba(x1))) | → | cc#(cc(ca(x1))) | (89) |
cc#(cb(ba(x1))) | → | cc#(ca(x1)) | (90) |
cc#(cb(ba(x1))) | → | ca#(x1) | (91) |
cc#(cb(bb(x1))) | → | ca#(ab(bc(cc(cc(cb(x1)))))) | (92) |
cc#(cb(bb(x1))) | → | ab#(bc(cc(cc(cb(x1))))) | (93) |
cc#(cb(bb(x1))) | → | bc#(cc(cc(cb(x1)))) | (94) |
cc#(cb(bb(x1))) | → | cc#(cc(cb(x1))) | (95) |
cc#(cb(bb(x1))) | → | cc#(cb(x1)) | (96) |
cc#(cb(bc(x1))) | → | ca#(ab(bc(cc(cc(cc(x1)))))) | (97) |
cc#(cb(bc(x1))) | → | ab#(bc(cc(cc(cc(x1))))) | (98) |
cc#(cb(bc(x1))) | → | bc#(cc(cc(cc(x1)))) | (99) |
cc#(cb(bc(x1))) | → | cc#(cc(cc(x1))) | (100) |
cc#(cb(bc(x1))) | → | cc#(cc(x1)) | (101) |
cc#(cb(bc(x1))) | → | cc#(x1) | (102) |
The dependency pairs are split into 1 component.
ac#(cb(ba(x1))) | → | ab#(bc(cc(cc(ca(x1))))) | (55) |
ab#(bc(x1)) | → | ac#(x1) | (54) |
ac#(cb(ba(x1))) | → | bc#(cc(cc(ca(x1)))) | (56) |
bc#(cb(ba(x1))) | → | ab#(bc(cc(cc(ca(x1))))) | (70) |
bc#(cb(ba(x1))) | → | bc#(cc(cc(ca(x1)))) | (71) |
bc#(cb(ba(x1))) | → | cc#(cc(ca(x1))) | (72) |
cc#(cb(ba(x1))) | → | ab#(bc(cc(cc(ca(x1))))) | (87) |
cc#(cb(ba(x1))) | → | bc#(cc(cc(ca(x1)))) | (88) |
bc#(cb(ba(x1))) | → | cc#(ca(x1)) | (73) |
cc#(cb(ba(x1))) | → | cc#(cc(ca(x1))) | (89) |
cc#(cb(ba(x1))) | → | cc#(ca(x1)) | (90) |
cc#(cb(bb(x1))) | → | ab#(bc(cc(cc(cb(x1))))) | (93) |
cc#(cb(bb(x1))) | → | bc#(cc(cc(cb(x1)))) | (94) |
bc#(cb(bb(x1))) | → | ab#(bc(cc(cc(cb(x1))))) | (76) |
bc#(cb(bb(x1))) | → | bc#(cc(cc(cb(x1)))) | (77) |
bc#(cb(bb(x1))) | → | cc#(cc(cb(x1))) | (78) |
cc#(cb(bb(x1))) | → | cc#(cc(cb(x1))) | (95) |
cc#(cb(bb(x1))) | → | cc#(cb(x1)) | (96) |
cc#(cb(bc(x1))) | → | ab#(bc(cc(cc(cc(x1))))) | (98) |
cc#(cb(bc(x1))) | → | bc#(cc(cc(cc(x1)))) | (99) |
bc#(cb(bb(x1))) | → | cc#(cb(x1)) | (79) |
cc#(cb(bc(x1))) | → | cc#(cc(cc(x1))) | (100) |
cc#(cb(bc(x1))) | → | cc#(cc(x1)) | (101) |
cc#(cb(bc(x1))) | → | cc#(x1) | (102) |
bc#(cb(bc(x1))) | → | ab#(bc(cc(cc(cc(x1))))) | (81) |
bc#(cb(bc(x1))) | → | bc#(cc(cc(cc(x1)))) | (82) |
bc#(cb(bc(x1))) | → | cc#(cc(cc(x1))) | (83) |
bc#(cb(bc(x1))) | → | cc#(cc(x1)) | (84) |
bc#(cb(bc(x1))) | → | cc#(x1) | (85) |
ac#(cb(ba(x1))) | → | cc#(cc(ca(x1))) | (57) |
ac#(cb(ba(x1))) | → | cc#(ca(x1)) | (58) |
ac#(cb(bb(x1))) | → | ab#(bc(cc(cc(cb(x1))))) | (60) |
ac#(cb(bb(x1))) | → | bc#(cc(cc(cb(x1)))) | (61) |
ac#(cb(bb(x1))) | → | cc#(cc(cb(x1))) | (62) |
ac#(cb(bb(x1))) | → | cc#(cb(x1)) | (63) |
ac#(cb(bc(x1))) | → | ab#(bc(cc(cc(cc(x1))))) | (64) |
ac#(cb(bc(x1))) | → | bc#(cc(cc(cc(x1)))) | (65) |
ac#(cb(bc(x1))) | → | cc#(cc(cc(x1))) | (66) |
ac#(cb(bc(x1))) | → | cc#(cc(x1)) | (67) |
ac#(cb(bc(x1))) | → | cc#(x1) | (68) |
[ac#(x1)] | = | 1 · x1 |
[cb(x1)] | = | 1 · x1 |
[ba(x1)] | = | 1 + 1 · x1 |
[ab#(x1)] | = | 1 · x1 |
[bc(x1)] | = | 1 + 1 · x1 |
[cc(x1)] | = | 1 · x1 |
[ca(x1)] | = | 1 · x1 |
[bc#(x1)] | = | 1 · x1 |
[cc#(x1)] | = | 1 · x1 |
[bb(x1)] | = | 1 + 1 · x1 |
[ab(x1)] | = | 1 · x1 |
[aa(x1)] | = | 1 + 1 · x1 |
[ac(x1)] | = | 1 + 1 · x1 |
ab#(bc(x1)) | → | ac#(x1) | (54) |
ac#(cb(ba(x1))) | → | bc#(cc(cc(ca(x1)))) | (56) |
bc#(cb(ba(x1))) | → | bc#(cc(cc(ca(x1)))) | (71) |
bc#(cb(ba(x1))) | → | cc#(cc(ca(x1))) | (72) |
cc#(cb(ba(x1))) | → | bc#(cc(cc(ca(x1)))) | (88) |
bc#(cb(ba(x1))) | → | cc#(ca(x1)) | (73) |
cc#(cb(ba(x1))) | → | cc#(cc(ca(x1))) | (89) |
cc#(cb(ba(x1))) | → | cc#(ca(x1)) | (90) |
cc#(cb(bb(x1))) | → | bc#(cc(cc(cb(x1)))) | (94) |
bc#(cb(bb(x1))) | → | bc#(cc(cc(cb(x1)))) | (77) |
bc#(cb(bb(x1))) | → | cc#(cc(cb(x1))) | (78) |
cc#(cb(bb(x1))) | → | cc#(cc(cb(x1))) | (95) |
cc#(cb(bb(x1))) | → | cc#(cb(x1)) | (96) |
cc#(cb(bc(x1))) | → | bc#(cc(cc(cc(x1)))) | (99) |
bc#(cb(bb(x1))) | → | cc#(cb(x1)) | (79) |
cc#(cb(bc(x1))) | → | cc#(cc(cc(x1))) | (100) |
cc#(cb(bc(x1))) | → | cc#(cc(x1)) | (101) |
cc#(cb(bc(x1))) | → | cc#(x1) | (102) |
bc#(cb(bc(x1))) | → | bc#(cc(cc(cc(x1)))) | (82) |
bc#(cb(bc(x1))) | → | cc#(cc(cc(x1))) | (83) |
bc#(cb(bc(x1))) | → | cc#(cc(x1)) | (84) |
bc#(cb(bc(x1))) | → | cc#(x1) | (85) |
ac#(cb(ba(x1))) | → | cc#(cc(ca(x1))) | (57) |
ac#(cb(ba(x1))) | → | cc#(ca(x1)) | (58) |
ac#(cb(bb(x1))) | → | bc#(cc(cc(cb(x1)))) | (61) |
ac#(cb(bb(x1))) | → | cc#(cc(cb(x1))) | (62) |
ac#(cb(bb(x1))) | → | cc#(cb(x1)) | (63) |
ac#(cb(bc(x1))) | → | bc#(cc(cc(cc(x1)))) | (65) |
ac#(cb(bc(x1))) | → | cc#(cc(cc(x1))) | (66) |
ac#(cb(bc(x1))) | → | cc#(cc(x1)) | (67) |
ac#(cb(bc(x1))) | → | cc#(x1) | (68) |
The dependency pairs are split into 0 components.