The rewrite relation of the following TRS is considered.
a(x1) | → | b(c(x1)) | (1) |
b(a(b(x1))) | → | x1 | (2) |
c(c(x1)) | → | a(a(a(b(x1)))) | (3) |
a(x1) | → | c(b(x1)) | (4) |
b(a(b(x1))) | → | x1 | (2) |
c(c(x1)) | → | b(a(a(a(x1)))) | (5) |
{a(☐), c(☐), b(☐)}
We obtain the transformed TRSa(a(x1)) | → | a(c(b(x1))) | (6) |
c(a(x1)) | → | c(c(b(x1))) | (7) |
b(a(x1)) | → | b(c(b(x1))) | (8) |
a(b(a(b(x1)))) | → | a(x1) | (9) |
c(b(a(b(x1)))) | → | c(x1) | (10) |
b(b(a(b(x1)))) | → | b(x1) | (11) |
a(c(c(x1))) | → | a(b(a(a(a(x1))))) | (12) |
c(c(c(x1))) | → | c(b(a(a(a(x1))))) | (13) |
b(c(c(x1))) | → | b(b(a(a(a(x1))))) | (14) |
Root-labeling is applied.
We obtain the labeled TRSaa(aa(x1)) | → | ac(cb(ba(x1))) | (15) |
aa(ac(x1)) | → | ac(cb(bc(x1))) | (16) |
aa(ab(x1)) | → | ac(cb(bb(x1))) | (17) |
ca(aa(x1)) | → | cc(cb(ba(x1))) | (18) |
ca(ac(x1)) | → | cc(cb(bc(x1))) | (19) |
ca(ab(x1)) | → | cc(cb(bb(x1))) | (20) |
ba(aa(x1)) | → | bc(cb(ba(x1))) | (21) |
ba(ac(x1)) | → | bc(cb(bc(x1))) | (22) |
ba(ab(x1)) | → | bc(cb(bb(x1))) | (23) |
ab(ba(ab(ba(x1)))) | → | aa(x1) | (24) |
ab(ba(ab(bc(x1)))) | → | ac(x1) | (25) |
ab(ba(ab(bb(x1)))) | → | ab(x1) | (26) |
cb(ba(ab(ba(x1)))) | → | ca(x1) | (27) |
cb(ba(ab(bc(x1)))) | → | cc(x1) | (28) |
cb(ba(ab(bb(x1)))) | → | cb(x1) | (29) |
bb(ba(ab(ba(x1)))) | → | ba(x1) | (30) |
bb(ba(ab(bc(x1)))) | → | bc(x1) | (31) |
bb(ba(ab(bb(x1)))) | → | bb(x1) | (32) |
ac(cc(ca(x1))) | → | ab(ba(aa(aa(aa(x1))))) | (33) |
ac(cc(cc(x1))) | → | ab(ba(aa(aa(ac(x1))))) | (34) |
ac(cc(cb(x1))) | → | ab(ba(aa(aa(ab(x1))))) | (35) |
cc(cc(ca(x1))) | → | cb(ba(aa(aa(aa(x1))))) | (36) |
cc(cc(cc(x1))) | → | cb(ba(aa(aa(ac(x1))))) | (37) |
cc(cc(cb(x1))) | → | cb(ba(aa(aa(ab(x1))))) | (38) |
bc(cc(ca(x1))) | → | bb(ba(aa(aa(aa(x1))))) | (39) |
bc(cc(cc(x1))) | → | bb(ba(aa(aa(ac(x1))))) | (40) |
bc(cc(cb(x1))) | → | bb(ba(aa(aa(ab(x1))))) | (41) |
[aa(x1)] | = | 1 · x1 + 1 |
[ac(x1)] | = | 1 · x1 + 2 |
[cb(x1)] | = | 1 · x1 |
[ba(x1)] | = | 1 · x1 |
[bc(x1)] | = | 1 · x1 + 1 |
[ab(x1)] | = | 1 · x1 + 1 |
[bb(x1)] | = | 1 · x1 |
[ca(x1)] | = | 1 · x1 + 1 |
[cc(x1)] | = | 1 · x1 + 2 |
ab(ba(ab(ba(x1)))) | → | aa(x1) | (24) |
ab(ba(ab(bc(x1)))) | → | ac(x1) | (25) |
ab(ba(ab(bb(x1)))) | → | ab(x1) | (26) |
cb(ba(ab(bb(x1)))) | → | cb(x1) | (29) |
bb(ba(ab(ba(x1)))) | → | ba(x1) | (30) |
bb(ba(ab(bc(x1)))) | → | bc(x1) | (31) |
bb(ba(ab(bb(x1)))) | → | bb(x1) | (32) |
ac(cc(ca(x1))) | → | ab(ba(aa(aa(aa(x1))))) | (33) |
ac(cc(cc(x1))) | → | ab(ba(aa(aa(ac(x1))))) | (34) |
cc(cc(ca(x1))) | → | cb(ba(aa(aa(aa(x1))))) | (36) |
cc(cc(cc(x1))) | → | cb(ba(aa(aa(ac(x1))))) | (37) |
cc(cc(cb(x1))) | → | cb(ba(aa(aa(ab(x1))))) | (38) |
bc(cc(ca(x1))) | → | bb(ba(aa(aa(aa(x1))))) | (39) |
bc(cc(cc(x1))) | → | bb(ba(aa(aa(ac(x1))))) | (40) |
aa#(aa(x1)) | → | ac#(cb(ba(x1))) | (42) |
aa#(aa(x1)) | → | cb#(ba(x1)) | (43) |
aa#(aa(x1)) | → | ba#(x1) | (44) |
aa#(ac(x1)) | → | ac#(cb(bc(x1))) | (45) |
aa#(ac(x1)) | → | cb#(bc(x1)) | (46) |
aa#(ac(x1)) | → | bc#(x1) | (47) |
aa#(ab(x1)) | → | ac#(cb(bb(x1))) | (48) |
aa#(ab(x1)) | → | cb#(bb(x1)) | (49) |
ca#(aa(x1)) | → | cb#(ba(x1)) | (50) |
ca#(aa(x1)) | → | ba#(x1) | (51) |
ca#(ac(x1)) | → | cb#(bc(x1)) | (52) |
ca#(ac(x1)) | → | bc#(x1) | (53) |
ca#(ab(x1)) | → | cb#(bb(x1)) | (54) |
ba#(aa(x1)) | → | bc#(cb(ba(x1))) | (55) |
ba#(aa(x1)) | → | cb#(ba(x1)) | (56) |
ba#(aa(x1)) | → | ba#(x1) | (57) |
ba#(ac(x1)) | → | bc#(cb(bc(x1))) | (58) |
ba#(ac(x1)) | → | cb#(bc(x1)) | (59) |
ba#(ac(x1)) | → | bc#(x1) | (60) |
ba#(ab(x1)) | → | bc#(cb(bb(x1))) | (61) |
ba#(ab(x1)) | → | cb#(bb(x1)) | (62) |
cb#(ba(ab(ba(x1)))) | → | ca#(x1) | (63) |
ac#(cc(cb(x1))) | → | ba#(aa(aa(ab(x1)))) | (64) |
ac#(cc(cb(x1))) | → | aa#(aa(ab(x1))) | (65) |
ac#(cc(cb(x1))) | → | aa#(ab(x1)) | (66) |
bc#(cc(cb(x1))) | → | ba#(aa(aa(ab(x1)))) | (67) |
bc#(cc(cb(x1))) | → | aa#(aa(ab(x1))) | (68) |
bc#(cc(cb(x1))) | → | aa#(ab(x1)) | (69) |
The dependency pairs are split into 1 component.
ac#(cc(cb(x1))) | → | ba#(aa(aa(ab(x1)))) | (64) |
ba#(aa(x1)) | → | bc#(cb(ba(x1))) | (55) |
bc#(cc(cb(x1))) | → | ba#(aa(aa(ab(x1)))) | (67) |
ba#(aa(x1)) | → | cb#(ba(x1)) | (56) |
cb#(ba(ab(ba(x1)))) | → | ca#(x1) | (63) |
ca#(aa(x1)) | → | cb#(ba(x1)) | (50) |
ca#(aa(x1)) | → | ba#(x1) | (51) |
ba#(aa(x1)) | → | ba#(x1) | (57) |
ba#(ac(x1)) | → | bc#(cb(bc(x1))) | (58) |
bc#(cc(cb(x1))) | → | aa#(aa(ab(x1))) | (68) |
aa#(aa(x1)) | → | ac#(cb(ba(x1))) | (42) |
ac#(cc(cb(x1))) | → | aa#(aa(ab(x1))) | (65) |
aa#(aa(x1)) | → | cb#(ba(x1)) | (43) |
aa#(aa(x1)) | → | ba#(x1) | (44) |
ba#(ac(x1)) | → | bc#(x1) | (60) |
aa#(ac(x1)) | → | ac#(cb(bc(x1))) | (45) |
aa#(ac(x1)) | → | bc#(x1) | (47) |
ca#(ac(x1)) | → | bc#(x1) | (53) |
[ac#(x1)] | = | 1 · x1 |
[cc(x1)] | = | 1 |
[cb(x1)] | = | 1 · x1 |
[ba#(x1)] | = | 1 |
[aa(x1)] | = | 0 |
[ab(x1)] | = | 0 |
[bc#(x1)] | = | 1 |
[ba(x1)] | = | 1 |
[cb#(x1)] | = | 1 |
[ca#(x1)] | = | 1 |
[ac(x1)] | = | 0 |
[bc(x1)] | = | 0 |
[aa#(x1)] | = | 1 |
[bb(x1)] | = | 0 |
[ca(x1)] | = | 1 |
ba(aa(x1)) | → | bc(cb(ba(x1))) | (21) |
ba(ac(x1)) | → | bc(cb(bc(x1))) | (22) |
ba(ab(x1)) | → | bc(cb(bb(x1))) | (23) |
cb(ba(ab(ba(x1)))) | → | ca(x1) | (27) |
cb(ba(ab(bc(x1)))) | → | cc(x1) | (28) |
bc(cc(cb(x1))) | → | bb(ba(aa(aa(ab(x1))))) | (41) |
ca(aa(x1)) | → | cc(cb(ba(x1))) | (18) |
ca(ac(x1)) | → | cc(cb(bc(x1))) | (19) |
ca(ab(x1)) | → | cc(cb(bb(x1))) | (20) |
aa#(ac(x1)) | → | ac#(cb(bc(x1))) | (45) |
[ac#(x1)] | = |
|
||||||||||||||||||
[cc(x1)] | = |
|
||||||||||||||||||
[cb(x1)] | = |
|
||||||||||||||||||
[ba#(x1)] | = |
|
||||||||||||||||||
[aa(x1)] | = |
|
||||||||||||||||||
[ab(x1)] | = |
|
||||||||||||||||||
[bc#(x1)] | = |
|
||||||||||||||||||
[ba(x1)] | = |
|
||||||||||||||||||
[cb#(x1)] | = |
|
||||||||||||||||||
[ca#(x1)] | = |
|
||||||||||||||||||
[ac(x1)] | = |
|
||||||||||||||||||
[bc(x1)] | = |
|
||||||||||||||||||
[aa#(x1)] | = |
|
||||||||||||||||||
[bb(x1)] | = |
|
||||||||||||||||||
[ca(x1)] | = |
|
ba#(ac(x1)) | → | bc#(cb(bc(x1))) | (58) |
[aa#(x1)] | = | -2 + 2 · x1 |
[ba#(x1)] | = | -2 + 2 · x1 |
[cb#(x1)] | = | -2 + 2 · x1 |
[ba(x1)] | = | 1 + x1 |
[bb(x1)] | = | -2 |
[ac#(x1)] | = | -2 + 2 · x1 |
[cb(x1)] | = | x1 |
[bc#(x1)] | = | -2 + 2 · x1 |
[aa(x1)] | = | 1 + x1 |
[ab(x1)] | = | x1 |
[ac(x1)] | = | 1 + x1 |
[bc(x1)] | = | 1 + x1 |
[ca(x1)] | = | 2 + x1 |
[cc(x1)] | = | 2 + x1 |
[ca#(x1)] | = | 1 + 2 · x1 |
cb#(ba(ab(ba(x1)))) | → | ca#(x1) | (63) |
ca#(aa(x1)) | → | cb#(ba(x1)) | (50) |
ca#(aa(x1)) | → | ba#(x1) | (51) |
bc#(cc(cb(x1))) | → | aa#(aa(ab(x1))) | (68) |
ac#(cc(cb(x1))) | → | aa#(aa(ab(x1))) | (65) |
ca#(ac(x1)) | → | bc#(x1) | (53) |
The dependency pairs are split into 1 component.
bc#(cc(cb(x1))) | → | ba#(aa(aa(ab(x1)))) | (67) |
ba#(aa(x1)) | → | bc#(cb(ba(x1))) | (55) |
ba#(aa(x1)) | → | ba#(x1) | (57) |
ba#(ac(x1)) | → | bc#(x1) | (60) |
[ba#(x1)] | = | -1 + x1 |
[bc#(x1)] | = | x1 |
[ba(x1)] | = | x1 |
[bb(x1)] | = | -2 |
[cb(x1)] | = | x1 |
[aa(x1)] | = | 1 + x1 |
[ab(x1)] | = | 1 + x1 |
[ac(x1)] | = | 2 + x1 |
[bc(x1)] | = | 1 + x1 |
[ca(x1)] | = | 1 + x1 |
[cc(x1)] | = | 2 + x1 |
ba#(ac(x1)) | → | bc#(x1) | (60) |
[ba#(x1)] | = | -1 + 2 · x1 |
[bc#(x1)] | = | 1 + 2 · x1 |
[ba(x1)] | = | x1 |
[bb(x1)] | = | -2 |
[cb(x1)] | = | x1 |
[aa(x1)] | = | 1 + x1 |
[ab(x1)] | = | 1 + x1 |
[ac(x1)] | = | 2 + x1 |
[bc(x1)] | = | 1 + x1 |
[ca(x1)] | = | 1 + x1 |
[cc(x1)] | = | 2 + x1 |
ba#(aa(x1)) | → | ba#(x1) | (57) |
[bc#(x1)] | = |
|
||||||||||||||||||
[cc(x1)] | = |
|
||||||||||||||||||
[cb(x1)] | = |
|
||||||||||||||||||
[ba#(x1)] | = |
|
||||||||||||||||||
[aa(x1)] | = |
|
||||||||||||||||||
[ab(x1)] | = |
|
||||||||||||||||||
[ba(x1)] | = |
|
||||||||||||||||||
[ac(x1)] | = |
|
||||||||||||||||||
[bb(x1)] | = |
|
||||||||||||||||||
[bc(x1)] | = |
|
||||||||||||||||||
[ca(x1)] | = |
|
bc#(cc(cb(x1))) | → | ba#(aa(aa(ab(x1)))) | (67) |
[ba#(x1)] | = | 1 + 1 · x1 |
[aa(x1)] | = | 0 |
[bc#(x1)] | = | 0 |
[cb(x1)] | = | 0 |
[ba(x1)] | = | 0 |
[bc(x1)] | = | 0 |
[ac(x1)] | = | 0 |
[ab(x1)] | = | 0 |
[bb(x1)] | = | 0 |
[ca(x1)] | = | 1 |
[cc(x1)] | = | 0 |
ba#(aa(x1)) | → | bc#(cb(ba(x1))) | (55) |
There are no pairs anymore.