The rewrite relation of the following TRS is considered.
a(b(x1)) | → | x1 | (1) |
a(c(x1)) | → | b(b(x1)) | (2) |
c(b(x1)) | → | a(a(c(c(x1)))) | (3) |
{c(☐), b(☐), a(☐)}
We obtain the transformed TRSc(a(b(x1))) | → | c(x1) | (4) |
c(a(c(x1))) | → | c(b(b(x1))) | (5) |
c(c(b(x1))) | → | c(a(a(c(c(x1))))) | (6) |
b(a(b(x1))) | → | b(x1) | (7) |
b(a(c(x1))) | → | b(b(b(x1))) | (8) |
b(c(b(x1))) | → | b(a(a(c(c(x1))))) | (9) |
a(a(b(x1))) | → | a(x1) | (10) |
a(a(c(x1))) | → | a(b(b(x1))) | (11) |
a(c(b(x1))) | → | a(a(a(c(c(x1))))) | (12) |
{c(☐), b(☐), a(☐)}
We obtain the transformed TRSc(c(a(b(x1)))) | → | c(c(x1)) | (13) |
c(c(a(c(x1)))) | → | c(c(b(b(x1)))) | (14) |
c(c(c(b(x1)))) | → | c(c(a(a(c(c(x1)))))) | (15) |
c(b(a(b(x1)))) | → | c(b(x1)) | (16) |
c(b(a(c(x1)))) | → | c(b(b(b(x1)))) | (17) |
c(b(c(b(x1)))) | → | c(b(a(a(c(c(x1)))))) | (18) |
c(a(a(b(x1)))) | → | c(a(x1)) | (19) |
c(a(a(c(x1)))) | → | c(a(b(b(x1)))) | (20) |
c(a(c(b(x1)))) | → | c(a(a(a(c(c(x1)))))) | (21) |
b(c(a(b(x1)))) | → | b(c(x1)) | (22) |
b(c(a(c(x1)))) | → | b(c(b(b(x1)))) | (23) |
b(c(c(b(x1)))) | → | b(c(a(a(c(c(x1)))))) | (24) |
b(b(a(b(x1)))) | → | b(b(x1)) | (25) |
b(b(a(c(x1)))) | → | b(b(b(b(x1)))) | (26) |
b(b(c(b(x1)))) | → | b(b(a(a(c(c(x1)))))) | (27) |
b(a(a(b(x1)))) | → | b(a(x1)) | (28) |
b(a(a(c(x1)))) | → | b(a(b(b(x1)))) | (29) |
b(a(c(b(x1)))) | → | b(a(a(a(c(c(x1)))))) | (30) |
a(c(a(b(x1)))) | → | a(c(x1)) | (31) |
a(c(a(c(x1)))) | → | a(c(b(b(x1)))) | (32) |
a(c(c(b(x1)))) | → | a(c(a(a(c(c(x1)))))) | (33) |
a(b(a(b(x1)))) | → | a(b(x1)) | (34) |
a(b(a(c(x1)))) | → | a(b(b(b(x1)))) | (35) |
a(b(c(b(x1)))) | → | a(b(a(a(c(c(x1)))))) | (36) |
a(a(a(b(x1)))) | → | a(a(x1)) | (37) |
a(a(a(c(x1)))) | → | a(a(b(b(x1)))) | (38) |
a(a(c(b(x1)))) | → | a(a(a(a(c(c(x1)))))) | (39) |
As carrier we take the set {0,...,8}. Symbols are labeled by the interpretation of their arguments using the interpretations (modulo 9):
[c(x1)] | = | 3x1 + 0 |
[b(x1)] | = | 3x1 + 1 |
[a(x1)] | = | 3x1 + 2 |
There are 243 ruless (increase limit for explicit display).
[c0(x1)] | = |
x1 +
|
||||
[c3(x1)] | = |
x1 +
|
||||
[c6(x1)] | = |
x1 +
|
||||
[c1(x1)] | = |
x1 +
|
||||
[c4(x1)] | = |
x1 +
|
||||
[c7(x1)] | = |
x1 +
|
||||
[c2(x1)] | = |
x1 +
|
||||
[c5(x1)] | = |
x1 +
|
||||
[c8(x1)] | = |
x1 +
|
||||
[b0(x1)] | = |
x1 +
|
||||
[b3(x1)] | = |
x1 +
|
||||
[b6(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[b4(x1)] | = |
x1 +
|
||||
[b7(x1)] | = |
x1 +
|
||||
[b2(x1)] | = |
x1 +
|
||||
[b5(x1)] | = |
x1 +
|
||||
[b8(x1)] | = |
x1 +
|
||||
[a0(x1)] | = |
x1 +
|
||||
[a3(x1)] | = |
x1 +
|
||||
[a6(x1)] | = |
x1 +
|
||||
[a1(x1)] | = |
x1 +
|
||||
[a4(x1)] | = |
x1 +
|
||||
[a7(x1)] | = |
x1 +
|
||||
[a2(x1)] | = |
x1 +
|
||||
[a5(x1)] | = |
x1 +
|
||||
[a8(x1)] | = |
x1 +
|
a8(a5(a7(b8(x1)))) | → | a8(a8(x1)) | (40) |
a8(a5(a7(b5(x1)))) | → | a8(a5(x1)) | (41) |
a8(a5(a7(b2(x1)))) | → | a8(a2(x1)) | (42) |
a8(a5(a4(b7(x1)))) | → | a5(a7(x1)) | (43) |
a8(a5(a4(b4(x1)))) | → | a5(a4(x1)) | (44) |
a8(a5(a1(b6(x1)))) | → | a2(a6(x1)) | (46) |
a8(a5(a1(b3(x1)))) | → | a2(a3(x1)) | (47) |
a8(a5(a1(b0(x1)))) | → | a2(a0(x1)) | (48) |
a7(b5(a7(b8(x1)))) | → | a7(b8(x1)) | (49) |
a7(b5(a7(b5(x1)))) | → | a7(b5(x1)) | (50) |
a7(b5(a7(b2(x1)))) | → | a7(b2(x1)) | (51) |
a7(b5(a4(b7(x1)))) | → | a4(b7(x1)) | (52) |
a7(b5(a4(b4(x1)))) | → | a4(b4(x1)) | (53) |
a7(b5(a4(b1(x1)))) | → | a4(b1(x1)) | (54) |
a7(b5(a1(b6(x1)))) | → | a1(b6(x1)) | (55) |
a7(b5(a1(b3(x1)))) | → | a1(b3(x1)) | (56) |
a7(b5(a1(b0(x1)))) | → | a1(b0(x1)) | (57) |
a6(c5(a7(b8(x1)))) | → | a6(c8(x1)) | (58) |
a6(c5(a7(b5(x1)))) | → | a6(c5(x1)) | (59) |
a6(c5(a7(b2(x1)))) | → | a6(c2(x1)) | (60) |
a6(c5(a1(b6(x1)))) | → | a0(c6(x1)) | (64) |
a6(c5(a1(b3(x1)))) | → | a0(c3(x1)) | (65) |
a6(c5(a1(b0(x1)))) | → | a0(c0(x1)) | (66) |
b8(a5(a7(b8(x1)))) | → | b8(a8(x1)) | (67) |
b8(a5(a7(b5(x1)))) | → | b8(a5(x1)) | (68) |
b8(a5(a7(b2(x1)))) | → | b8(a2(x1)) | (69) |
b8(a5(a4(b7(x1)))) | → | b5(a7(x1)) | (70) |
b8(a5(a4(b4(x1)))) | → | b5(a4(x1)) | (71) |
b7(b5(a7(b8(x1)))) | → | b7(b8(x1)) | (76) |
b7(b5(a7(b5(x1)))) | → | b7(b5(x1)) | (77) |
b7(b5(a7(b2(x1)))) | → | b7(b2(x1)) | (78) |
b7(b5(a1(b6(x1)))) | → | b1(b6(x1)) | (82) |
b7(b5(a1(b3(x1)))) | → | b1(b3(x1)) | (83) |
b7(b5(a1(b0(x1)))) | → | b1(b0(x1)) | (84) |
b6(c5(a7(b8(x1)))) | → | b6(c8(x1)) | (85) |
b6(c5(a7(b5(x1)))) | → | b6(c5(x1)) | (86) |
b6(c5(a7(b2(x1)))) | → | b6(c2(x1)) | (87) |
b6(c5(a1(b6(x1)))) | → | b0(c6(x1)) | (91) |
b6(c5(a1(b3(x1)))) | → | b0(c3(x1)) | (92) |
b6(c5(a1(b0(x1)))) | → | b0(c0(x1)) | (93) |
c8(a5(a7(b8(x1)))) | → | c8(a8(x1)) | (94) |
c8(a5(a7(b5(x1)))) | → | c8(a5(x1)) | (95) |
c8(a5(a7(b2(x1)))) | → | c8(a2(x1)) | (96) |
c8(a5(a4(b7(x1)))) | → | c5(a7(x1)) | (97) |
c8(a5(a4(b4(x1)))) | → | c5(a4(x1)) | (98) |
c7(b5(a7(b8(x1)))) | → | c7(b8(x1)) | (103) |
c7(b5(a7(b5(x1)))) | → | c7(b5(x1)) | (104) |
c7(b5(a7(b2(x1)))) | → | c7(b2(x1)) | (105) |
c7(b5(a1(b6(x1)))) | → | c1(b6(x1)) | (109) |
c7(b5(a1(b3(x1)))) | → | c1(b3(x1)) | (110) |
c7(b5(a1(b0(x1)))) | → | c1(b0(x1)) | (111) |
c6(c5(a7(b8(x1)))) | → | c6(c8(x1)) | (112) |
c6(c5(a7(b5(x1)))) | → | c6(c5(x1)) | (113) |
c6(c5(a7(b2(x1)))) | → | c6(c2(x1)) | (114) |
c6(c5(a1(b6(x1)))) | → | c0(c6(x1)) | (118) |
c6(c5(a1(b3(x1)))) | → | c0(c3(x1)) | (119) |
c6(c5(a1(b0(x1)))) | → | c0(c0(x1)) | (120) |
a7(b2(a6(c8(x1)))) | → | a4(b4(b7(b8(x1)))) | (130) |
a7(b2(a6(c5(x1)))) | → | a4(b4(b7(b5(x1)))) | (131) |
a7(b2(a6(c2(x1)))) | → | a4(b4(b7(b2(x1)))) | (132) |
a7(b2(a3(c7(x1)))) | → | a4(b4(b4(b7(x1)))) | (133) |
a7(b2(a3(c4(x1)))) | → | a4(b4(b4(b4(x1)))) | (134) |
a7(b2(a3(c1(x1)))) | → | a4(b4(b4(b1(x1)))) | (135) |
a7(b2(a0(c6(x1)))) | → | a4(b4(b1(b6(x1)))) | (136) |
a7(b2(a0(c3(x1)))) | → | a4(b4(b1(b3(x1)))) | (137) |
a7(b2(a0(c0(x1)))) | → | a4(b4(b1(b0(x1)))) | (138) |
a1(b3(c7(b8(x1)))) | → | a7(b8(a2(a0(c6(c8(x1)))))) | (211) |
a1(b3(c7(b5(x1)))) | → | a7(b8(a2(a0(c6(c5(x1)))))) | (212) |
a1(b3(c7(b2(x1)))) | → | a7(b8(a2(a0(c6(c2(x1)))))) | (213) |
a1(b3(c4(b7(x1)))) | → | a7(b8(a2(a0(c3(c7(x1)))))) | (214) |
a1(b3(c4(b4(x1)))) | → | a7(b8(a2(a0(c3(c4(x1)))))) | (215) |
a1(b3(c4(b1(x1)))) | → | a7(b8(a2(a0(c3(c1(x1)))))) | (216) |
a1(b3(c1(b6(x1)))) | → | a7(b8(a2(a0(c0(c6(x1)))))) | (217) |
a1(b3(c1(b3(x1)))) | → | a7(b8(a2(a0(c0(c3(x1)))))) | (218) |
a1(b3(c1(b0(x1)))) | → | a7(b8(a2(a0(c0(c0(x1)))))) | (219) |
b2(a3(c7(b8(x1)))) | → | b8(a8(a2(a0(c6(c8(x1)))))) | (229) |
b2(a3(c7(b5(x1)))) | → | b8(a8(a2(a0(c6(c5(x1)))))) | (230) |
b2(a3(c7(b2(x1)))) | → | b8(a8(a2(a0(c6(c2(x1)))))) | (231) |
b2(a3(c4(b7(x1)))) | → | b8(a8(a2(a0(c3(c7(x1)))))) | (232) |
b2(a3(c4(b4(x1)))) | → | b8(a8(a2(a0(c3(c4(x1)))))) | (233) |
b2(a3(c4(b1(x1)))) | → | b8(a8(a2(a0(c3(c1(x1)))))) | (234) |
b2(a3(c1(b6(x1)))) | → | b8(a8(a2(a0(c0(c6(x1)))))) | (235) |
b2(a3(c1(b3(x1)))) | → | b8(a8(a2(a0(c0(c3(x1)))))) | (236) |
b2(a3(c1(b0(x1)))) | → | b8(a8(a2(a0(c0(c0(x1)))))) | (237) |
c2(a3(c7(b8(x1)))) | → | c8(a8(a2(a0(c6(c8(x1)))))) | (256) |
c2(a3(c7(b5(x1)))) | → | c8(a8(a2(a0(c6(c5(x1)))))) | (257) |
c2(a3(c7(b2(x1)))) | → | c8(a8(a2(a0(c6(c2(x1)))))) | (258) |
c2(a3(c4(b7(x1)))) | → | c8(a8(a2(a0(c3(c7(x1)))))) | (259) |
c2(a3(c4(b4(x1)))) | → | c8(a8(a2(a0(c3(c4(x1)))))) | (260) |
c2(a3(c4(b1(x1)))) | → | c8(a8(a2(a0(c3(c1(x1)))))) | (261) |
c2(a3(c1(b6(x1)))) | → | c8(a8(a2(a0(c0(c6(x1)))))) | (262) |
c2(a3(c1(b3(x1)))) | → | c8(a8(a2(a0(c0(c3(x1)))))) | (263) |
c2(a3(c1(b0(x1)))) | → | c8(a8(a2(a0(c0(c0(x1)))))) | (264) |
[c0(x1)] | = |
|
||||||||
[c3(x1)] | = |
|
||||||||
[c6(x1)] | = |
|
||||||||
[c1(x1)] | = |
|
||||||||
[c4(x1)] | = |
|
||||||||
[c7(x1)] | = |
|
||||||||
[c2(x1)] | = |
|
||||||||
[c5(x1)] | = |
|
||||||||
[c8(x1)] | = |
|
||||||||
[b0(x1)] | = |
|
||||||||
[b3(x1)] | = |
|
||||||||
[b6(x1)] | = |
|
||||||||
[b1(x1)] | = |
|
||||||||
[b4(x1)] | = |
|
||||||||
[b7(x1)] | = |
|
||||||||
[b2(x1)] | = |
|
||||||||
[b5(x1)] | = |
|
||||||||
[b8(x1)] | = |
|
||||||||
[a0(x1)] | = |
|
||||||||
[a3(x1)] | = |
|
||||||||
[a6(x1)] | = |
|
||||||||
[a1(x1)] | = |
|
||||||||
[a4(x1)] | = |
|
||||||||
[a2(x1)] | = |
|
||||||||
[a5(x1)] | = |
|
||||||||
[a8(x1)] | = |
|
a8(a5(a4(b1(x1)))) | → | a5(a1(x1)) | (45) |
a6(c5(a4(b7(x1)))) | → | a3(c7(x1)) | (61) |
a6(c5(a4(b4(x1)))) | → | a3(c4(x1)) | (62) |
a6(c5(a4(b1(x1)))) | → | a3(c1(x1)) | (63) |
b8(a5(a4(b1(x1)))) | → | b5(a1(x1)) | (72) |
b7(b5(a4(b7(x1)))) | → | b4(b7(x1)) | (79) |
b7(b5(a4(b4(x1)))) | → | b4(b4(x1)) | (80) |
b7(b5(a4(b1(x1)))) | → | b4(b1(x1)) | (81) |
b6(c5(a4(b7(x1)))) | → | b3(c7(x1)) | (88) |
b6(c5(a4(b4(x1)))) | → | b3(c4(x1)) | (89) |
b6(c5(a4(b1(x1)))) | → | b3(c1(x1)) | (90) |
c8(a5(a4(b1(x1)))) | → | c5(a1(x1)) | (99) |
c7(b5(a4(b7(x1)))) | → | c4(b7(x1)) | (106) |
c7(b5(a4(b4(x1)))) | → | c4(b4(x1)) | (107) |
c7(b5(a4(b1(x1)))) | → | c4(b1(x1)) | (108) |
c6(c5(a4(b7(x1)))) | → | c3(c7(x1)) | (115) |
c6(c5(a4(b4(x1)))) | → | c3(c4(x1)) | (116) |
c6(c5(a4(b1(x1)))) | → | c3(c1(x1)) | (117) |
[c0(x1)] | = |
x1 +
|
||||
[c3(x1)] | = |
x1 +
|
||||
[c6(x1)] | = |
x1 +
|
||||
[c1(x1)] | = |
x1 +
|
||||
[c4(x1)] | = |
x1 +
|
||||
[c7(x1)] | = |
x1 +
|
||||
[c2(x1)] | = |
x1 +
|
||||
[c5(x1)] | = |
x1 +
|
||||
[c8(x1)] | = |
x1 +
|
||||
[b0(x1)] | = |
x1 +
|
||||
[b3(x1)] | = |
x1 +
|
||||
[b6(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[b4(x1)] | = |
x1 +
|
||||
[b7(x1)] | = |
x1 +
|
||||
[b2(x1)] | = |
x1 +
|
||||
[b5(x1)] | = |
x1 +
|
||||
[b8(x1)] | = |
x1 +
|
||||
[a0(x1)] | = |
x1 +
|
||||
[a3(x1)] | = |
x1 +
|
||||
[a6(x1)] | = |
x1 +
|
||||
[a1(x1)] | = |
x1 +
|
||||
[a4(x1)] | = |
x1 +
|
||||
[a2(x1)] | = |
x1 +
|
||||
[a5(x1)] | = |
x1 +
|
||||
[a8(x1)] | = |
x1 +
|
There are 132 ruless (increase limit for explicit display).
There are no rules in the TRS. Hence, it is terminating.