The rewrite relation of the following TRS is considered.
a(b(a(a(b(a(x1)))))) | → | a(a(b(a(b(a(b(a(b(a(b(a(a(b(x1)))))))))))))) | (1) |
{b(☐), a(☐)}
We obtain the transformed TRSb(a(b(a(a(b(a(x1))))))) | → | b(a(a(b(a(b(a(b(a(b(a(b(a(a(b(x1))))))))))))))) | (2) |
a(a(b(a(a(b(a(x1))))))) | → | a(a(a(b(a(b(a(b(a(b(a(b(a(a(b(x1))))))))))))))) | (3) |
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(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (4) |
a1(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (5) |
b1(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (6) |
b1(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (7) |
b1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1)))))))))))) | (8) |
b1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1)))))))))) | (9) |
b1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b0(x1)))))))) | (10) |
b1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a0(b1(a1(a0(b0(x1)))))) | (11) |
b1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a1(a0(b0(x1)))) | (12) |
b1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (13) |
b1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1#(a0(b0(x1))) | (14) |
b1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1)))))))))))))) | (15) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (16) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (17) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (18) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (19) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (20) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(x1)))) | (21) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (22) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (23) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (24) |
a1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1)))))))))))) | (25) |
a1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1)))))))))) | (26) |
a1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b0(x1)))))))) | (27) |
a1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a0(b1(a1(a0(b0(x1)))))) | (28) |
a1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1#(a1(a0(b0(x1)))) | (29) |
a1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1#(a0(b0(x1))) | (30) |
a1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1)))))))))))))) | (31) |
a1#(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1#(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (32) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (33) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (34) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (35) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (36) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (37) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(x1)))) | (38) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (39) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (40) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (41) |
The dependency pairs are split into 1 component.
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(x1)))) | (38) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (16) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (17) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (18) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (19) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (20) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(x1)))) | (21) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (22) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (23) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (33) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (24) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (34) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (35) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (36) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (37) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (39) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (40) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (41) |
[b0(x1)] | = |
|
||||||||||||
[b1(x1)] | = |
|
||||||||||||
[a0(x1)] | = |
|
||||||||||||
[a1(x1)] | = |
|
||||||||||||
[b1#(x1)] | = |
|
||||||||||||
[a1#(x1)] | = |
|
a1(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (4) |
a1(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (5) |
b1(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (6) |
b1(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (7) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (41) |
The dependency pairs are split into 1 component.
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(x1)))) | (38) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (16) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (17) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (18) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (19) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (20) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(x1)))) | (21) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (22) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (23) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (33) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (24) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (34) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (35) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (36) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (37) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (39) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (40) |
[b0(x1)] | = |
|
||||||||||||
[b1(x1)] | = |
|
||||||||||||
[a0(x1)] | = |
|
||||||||||||
[a1(x1)] | = |
|
||||||||||||
[b1#(x1)] | = |
|
||||||||||||
[a1#(x1)] | = |
|
a1(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (4) |
a1(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (5) |
b1(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (6) |
b1(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (7) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(x1)))) | (38) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(x1)))) | (21) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (22) |
The dependency pairs are split into 1 component.
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (16) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (17) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (18) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (19) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (20) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (23) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (33) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (24) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (34) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (35) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (36) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (37) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (39) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (40) |
[b0(x1)] | = |
|
||||||||||||||||||
[b1(x1)] | = |
|
||||||||||||||||||
[a0(x1)] | = |
|
||||||||||||||||||
[a1(x1)] | = |
|
||||||||||||||||||
[b1#(x1)] | = |
|
||||||||||||||||||
[a1#(x1)] | = |
|
a1(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (4) |
a1(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (5) |
b1(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (6) |
b1(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (7) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (16) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (17) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (18) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (19) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (20) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(x1) | (33) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))) | (34) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))) | (35) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a0(b1(a1(a0(b1(x1)))))))) | (36) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1#(a0(b1(a1(a0(b1(x1)))))) | (37) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (39) |
a1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (40) |
[b0(x1)] | = |
x1 +
|
||||
[b1(x1)] | = |
x1 +
|
||||
[a0(x1)] | = |
x1 +
|
||||
[a1(x1)] | = |
x1 +
|
||||
[b1#(x1)] | = |
x1 +
|
||||
[a1#(x1)] | = |
x1 +
|
a1(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (4) |
a1(a0(b1(a1(a0(b1(a0(x1))))))) | → | a1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (5) |
b1(a0(b1(a1(a0(b1(a1(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1))))))))))))))) | (6) |
b1(a0(b1(a1(a0(b1(a0(x1))))))) | → | b1(a1(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b0(x1))))))))))))))) | (7) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(x1))) | (23) |
b1#(a0(b1(a1(a0(b1(a1(x1))))))) | → | a1#(a0(b1(a0(b1(a0(b1(a0(b1(a0(b1(a1(a0(b1(x1)))))))))))))) | (24) |
The dependency pairs are split into 0 components.