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