The rewrite relation of the following TRS is considered.
As carrier we take the set
{0,...,7}.
Symbols are labeled by the interpretation of their arguments using the interpretations
(modulo 8):
b0(b4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(16) |
b0(b4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(17) |
b0(b4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(18) |
b0(b4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(19) |
b0(b4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(20) |
b0(b4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(21) |
b0(b4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(22) |
b0(b4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(23) |
b2(b5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(24) |
b2(b5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(25) |
b2(b5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(26) |
b2(b5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(27) |
b2(b5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(28) |
b2(b5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(29) |
b2(b5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(30) |
b2(b5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(31) |
b1(a4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(32) |
b1(a4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(33) |
b1(a4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(34) |
b1(a4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(35) |
b1(a4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(36) |
b1(a4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(37) |
b1(a4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(38) |
b1(a4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(39) |
b3(a5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(40) |
b3(a5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(41) |
b3(a5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(42) |
b3(a5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(43) |
b3(a5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(44) |
b3(a5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(45) |
b3(a5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(46) |
b3(a5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(47) |
a0(b4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(48) |
a0(b4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(49) |
a0(b4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(50) |
a0(b4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(51) |
a0(b4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(52) |
a0(b4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(53) |
a0(b4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(54) |
a0(b4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(55) |
a2(b5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(56) |
a2(b5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(57) |
a2(b5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(58) |
a2(b5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(59) |
a2(b5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(60) |
a2(b5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(61) |
a2(b5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(62) |
a2(b5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(63) |
a1(a4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(64) |
a1(a4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(65) |
a1(a4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(66) |
a1(a4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(67) |
a1(a4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(68) |
a1(a4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(69) |
a1(a4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(70) |
a1(a4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(71) |
a3(a5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(72) |
a3(a5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(73) |
a3(a5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(74) |
a3(a5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(75) |
a3(a5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(76) |
a3(a5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(77) |
a3(a5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(78) |
a3(a5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(79) |
b0(b4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(16) |
b0(b4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(17) |
b0(b4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(18) |
b0(b4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(19) |
b0(b4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(20) |
b0(b4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(21) |
b0(b4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(22) |
b0(b4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
b4(b2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(23) |
b2(b5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(24) |
b2(b5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(25) |
b2(b5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(26) |
b2(b5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(27) |
b2(b5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(28) |
b2(b5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(29) |
b2(b5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(30) |
b2(b5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
b6(b3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(31) |
b1(a4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(32) |
b1(a4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(33) |
b1(a4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(34) |
b1(a4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(35) |
b1(a4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(36) |
b1(a4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(37) |
b1(a4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(38) |
b1(a4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
b5(a2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(39) |
b3(a5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(40) |
b3(a5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(41) |
b3(a5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(42) |
b3(a5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(43) |
b3(a5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(44) |
b3(a5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(45) |
b3(a5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(46) |
b3(a5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
b7(a3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(47) |
a0(b4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(48) |
a0(b4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(49) |
a0(b4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(50) |
a0(b4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(51) |
a0(b4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(52) |
a0(b4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(53) |
a0(b4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(54) |
a0(b4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
a4(b2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(55) |
a2(b5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(56) |
a2(b5(a2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(57) |
a2(b5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(58) |
a2(b5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(59) |
a2(b5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(60) |
a2(b5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(61) |
a2(b5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(62) |
a2(b5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
a6(b3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(63) |
a1(a4(b2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(64) |
a1(a4(b2(b1(a4(b2(b1(a0(b4(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b2(b1(a4(x1)))))))))) |
(65) |
a1(a4(b2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(66) |
a1(a4(b2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(67) |
a1(a4(b2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(68) |
a1(a4(b2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(69) |
a1(a4(b2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(70) |
a1(a4(b2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
a5(a2(b5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(71) |
a3(a5(a2(b1(a4(b2(b1(a0(b0(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b2(b1(a0(x1)))))))))) |
(72) |
a3(a5(a2(b1(a4(b2(b1(a4(b2(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b2(b5(a2(x1)))))))))) |
(74) |
a3(a5(a2(b1(a4(b2(b1(a4(b6(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b2(b5(a6(x1)))))))))) |
(75) |
a3(a5(a2(b1(a4(b2(b5(a2(b1(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b6(b3(a1(x1)))))))))) |
(76) |
a3(a5(a2(b1(a4(b2(b5(a2(b5(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b6(b3(a5(x1)))))))))) |
(77) |
a3(a5(a2(b1(a4(b2(b5(a6(b3(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b6(b7(a3(x1)))))))))) |
(78) |
a3(a5(a2(b1(a4(b2(b5(a6(b7(x1))))))))) |
→ |
a7(a3(a5(a2(b1(a0(b4(b6(b7(a7(x1)))))))))) |
(79) |
There are no rules.
There are no rules in the TRS. Hence, it is terminating.