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):
There are 128 ruless (increase limit for explicit display).
a6(a5(b3(a6(a5(x1))))) |
→ |
b6(a4(a1(x1))) |
(159) |
a2(a5(b3(a6(a5(x1))))) |
→ |
b2(a4(a1(x1))) |
(160) |
a6(a5(b3(a6(b5(x1))))) |
→ |
b6(a4(b1(x1))) |
(161) |
a2(a5(b3(a6(b5(x1))))) |
→ |
b2(a4(b1(x1))) |
(162) |
a7(b7(b6(a4(a1(a3(a7(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) |
(163) |
a3(b7(b6(a4(a1(a3(a7(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) |
(164) |
a5(b3(b6(a4(a1(a3(a7(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) |
(165) |
a1(b3(b6(a4(a1(a3(a7(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) |
(166) |
a6(b5(b2(a4(a1(a3(a7(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) |
(167) |
a2(b5(b2(a4(a1(a3(a7(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) |
(168) |
a0(b1(b2(a4(a1(a3(a7(x1))))))) |
→ |
b0(b0(a0(b1(a2(a5(a3(a7(a7(x1))))))))) |
(169) |
a7(b7(b6(a4(b1(a2(a5(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) |
(170) |
a3(b7(b6(a4(b1(a2(a5(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) |
(171) |
a5(b3(b6(a4(b1(a2(a5(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) |
(172) |
a1(b3(b6(a4(b1(a2(a5(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) |
(173) |
a6(b5(b2(a4(b1(a2(a5(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) |
(174) |
a2(b5(b2(a4(b1(a2(a5(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) |
(175) |
a0(b1(b2(a4(b1(a2(a5(x1))))))) |
→ |
b0(b0(a0(b1(a2(a5(b3(a6(a5(x1))))))))) |
(176) |
a7(b7(b6(a4(a1(b3(a6(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) |
(177) |
a3(b7(b6(a4(a1(b3(a6(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) |
(178) |
a5(b3(b6(a4(a1(b3(a6(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) |
(179) |
a1(b3(b6(a4(a1(b3(a6(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) |
(180) |
a6(b5(b2(a4(a1(b3(a6(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) |
(181) |
a2(b5(b2(a4(a1(b3(a6(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) |
(182) |
a0(b1(b2(a4(a1(b3(a6(x1))))))) |
→ |
b0(b0(a0(b1(a2(a5(a3(b7(a6(x1))))))))) |
(183) |
a7(b7(b6(a4(b1(b2(a4(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) |
(184) |
a3(b7(b6(a4(b1(b2(a4(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) |
(185) |
a5(b3(b6(a4(b1(b2(a4(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) |
(186) |
a1(b3(b6(a4(b1(b2(a4(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) |
(187) |
a6(b5(b2(a4(b1(b2(a4(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) |
(188) |
a2(b5(b2(a4(b1(b2(a4(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) |
(189) |
a0(b1(b2(a4(b1(b2(a4(x1))))))) |
→ |
b0(b0(a0(b1(a2(a5(b3(b6(a4(x1))))))))) |
(190) |
a7(b7(b6(a4(a1(a3(b7(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) |
(191) |
a3(b7(b6(a4(a1(a3(b7(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) |
(192) |
a5(b3(b6(a4(a1(a3(b7(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) |
(193) |
a1(b3(b6(a4(a1(a3(b7(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) |
(194) |
a6(b5(b2(a4(a1(a3(b7(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) |
(195) |
a2(b5(b2(a4(a1(a3(b7(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) |
(196) |
a0(b1(b2(a4(a1(a3(b7(x1))))))) |
→ |
b0(b0(a0(b1(a2(a5(a3(a7(b7(x1))))))))) |
(197) |
a7(b7(b6(a4(b1(a2(b5(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) |
(198) |
a3(b7(b6(a4(b1(a2(b5(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) |
(199) |
a5(b3(b6(a4(b1(a2(b5(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) |
(200) |
a1(b3(b6(a4(b1(a2(b5(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) |
(201) |
a6(b5(b2(a4(b1(a2(b5(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) |
(202) |
a2(b5(b2(a4(b1(a2(b5(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) |
(203) |
a0(b1(b2(a4(b1(a2(b5(x1))))))) |
→ |
b0(b0(a0(b1(a2(a5(b3(a6(b5(x1))))))))) |
(204) |
a7(b7(b6(a4(a1(b3(b6(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) |
(205) |
a3(b7(b6(a4(a1(b3(b6(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) |
(206) |
a5(b3(b6(a4(a1(b3(b6(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) |
(207) |
a1(b3(b6(a4(a1(b3(b6(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) |
(208) |
a6(b5(b2(a4(a1(b3(b6(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) |
(209) |
a2(b5(b2(a4(a1(b3(b6(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) |
(210) |
a0(b1(b2(a4(a1(b3(b6(x1))))))) |
→ |
b0(b0(a0(b1(a2(a5(a3(b7(b6(x1))))))))) |
(211) |
a7(b7(b6(a4(b1(b2(b4(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) |
(212) |
a3(b7(b6(a4(b1(b2(b4(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) |
(213) |
a5(b3(b6(a4(b1(b2(b4(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) |
(214) |
a1(b3(b6(a4(b1(b2(b4(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) |
(215) |
a6(b5(b2(a4(b1(b2(b4(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) |
(216) |
a2(b5(b2(a4(b1(b2(b4(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) |
(217) |
a0(b1(b2(a4(b1(b2(b4(x1))))))) |
→ |
b0(b0(a0(b1(a2(a5(b3(b6(b4(x1))))))))) |
(218) |
a7(b7(b6(a4(a1(a3(a7(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) |
(163) |
a3(b7(b6(a4(a1(a3(a7(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(a3(a7(a7(x1))))))))) |
(164) |
a5(b3(b6(a4(a1(a3(a7(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) |
(165) |
a1(b3(b6(a4(a1(a3(a7(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(a3(a7(a7(x1))))))))) |
(166) |
a6(b5(b2(a4(a1(a3(a7(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) |
(167) |
a2(b5(b2(a4(a1(a3(a7(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(a3(a7(a7(x1))))))))) |
(168) |
a7(b7(b6(a4(b1(a2(a5(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) |
(170) |
a3(b7(b6(a4(b1(a2(a5(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(b3(a6(a5(x1))))))))) |
(171) |
a5(b3(b6(a4(b1(a2(a5(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) |
(172) |
a1(b3(b6(a4(b1(a2(a5(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(b3(a6(a5(x1))))))))) |
(173) |
a6(b5(b2(a4(b1(a2(a5(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) |
(174) |
a2(b5(b2(a4(b1(a2(a5(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(b3(a6(a5(x1))))))))) |
(175) |
a7(b7(b6(a4(a1(b3(a6(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) |
(177) |
a3(b7(b6(a4(a1(b3(a6(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(a3(b7(a6(x1))))))))) |
(178) |
a5(b3(b6(a4(a1(b3(a6(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) |
(179) |
a1(b3(b6(a4(a1(b3(a6(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(a3(b7(a6(x1))))))))) |
(180) |
a6(b5(b2(a4(a1(b3(a6(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) |
(181) |
a2(b5(b2(a4(a1(b3(a6(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(a3(b7(a6(x1))))))))) |
(182) |
a7(b7(b6(a4(b1(b2(a4(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) |
(184) |
a3(b7(b6(a4(b1(b2(a4(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(b3(b6(a4(x1))))))))) |
(185) |
a1(b3(b6(a4(b1(b2(a4(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(b3(b6(a4(x1))))))))) |
(187) |
a6(b5(b2(a4(b1(b2(a4(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) |
(188) |
a2(b5(b2(a4(b1(b2(a4(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(b3(b6(a4(x1))))))))) |
(189) |
a7(b7(b6(a4(a1(a3(b7(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) |
(191) |
a3(b7(b6(a4(a1(a3(b7(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(a3(a7(b7(x1))))))))) |
(192) |
a5(b3(b6(a4(a1(a3(b7(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) |
(193) |
a1(b3(b6(a4(a1(a3(b7(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(a3(a7(b7(x1))))))))) |
(194) |
a6(b5(b2(a4(a1(a3(b7(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) |
(195) |
a2(b5(b2(a4(a1(a3(b7(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(a3(a7(b7(x1))))))))) |
(196) |
a7(b7(b6(a4(b1(a2(b5(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) |
(198) |
a3(b7(b6(a4(b1(a2(b5(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(b3(a6(b5(x1))))))))) |
(199) |
a5(b3(b6(a4(b1(a2(b5(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) |
(200) |
a1(b3(b6(a4(b1(a2(b5(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(b3(a6(b5(x1))))))))) |
(201) |
a6(b5(b2(a4(b1(a2(b5(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) |
(202) |
a2(b5(b2(a4(b1(a2(b5(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(b3(a6(b5(x1))))))))) |
(203) |
a7(b7(b6(a4(a1(b3(b6(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) |
(205) |
a3(b7(b6(a4(a1(b3(b6(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(a3(b7(b6(x1))))))))) |
(206) |
a5(b3(b6(a4(a1(b3(b6(x1))))))) |
→ |
b5(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) |
(207) |
a1(b3(b6(a4(a1(b3(b6(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(a3(b7(b6(x1))))))))) |
(208) |
a6(b5(b2(a4(a1(b3(b6(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) |
(209) |
a2(b5(b2(a4(a1(b3(b6(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(a3(b7(b6(x1))))))))) |
(210) |
a7(b7(b6(a4(b1(b2(b4(x1))))))) |
→ |
b7(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) |
(212) |
a3(b7(b6(a4(b1(b2(b4(x1))))))) |
→ |
b3(b6(a4(b1(a2(a5(b3(b6(b4(x1))))))))) |
(213) |
a1(b3(b6(a4(b1(b2(b4(x1))))))) |
→ |
b1(b2(a4(b1(a2(a5(b3(b6(b4(x1))))))))) |
(215) |
a6(b5(b2(a4(b1(b2(b4(x1))))))) |
→ |
b6(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) |
(216) |
a2(b5(b2(a4(b1(b2(b4(x1))))))) |
→ |
b2(b4(a0(b1(a2(a5(b3(b6(b4(x1))))))))) |
(217) |
There are no rules in the TRS. Hence, it is terminating.
As carrier we take the set
{0,...,7}.
Symbols are labeled by the interpretation of their arguments using the interpretations
(modulo 8):
a7(a3(a1(a4(b6(b7(a7(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(95) |
a7(a3(a1(a4(b6(b7(a3(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(96) |
a7(a3(a1(a4(b6(b3(a5(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(97) |
a7(a3(a1(a4(b6(b3(a1(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(98) |
a7(a3(a1(a4(b2(b5(a6(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(99) |
a7(a3(a1(a4(b2(b5(a2(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(100) |
a7(a3(a1(a4(b2(b1(a4(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(101) |
a7(a3(a1(a4(b2(b1(a0(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(102) |
a5(a2(b1(a4(b6(b7(a7(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(103) |
a5(a2(b1(a4(b6(b7(a3(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(104) |
a5(a2(b1(a4(b6(b3(a5(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(105) |
a5(a2(b1(a4(b6(b3(a1(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(106) |
a5(a2(b1(a4(b2(b5(a6(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(107) |
a5(a2(b1(a4(b2(b5(a2(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(108) |
a5(a2(b1(a4(b2(b1(a4(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(109) |
a5(a2(b1(a4(b2(b1(a0(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(110) |
a6(b3(a1(a4(b6(b7(a7(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(111) |
a6(b3(a1(a4(b6(b7(a3(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(112) |
a6(b3(a1(a4(b6(b3(a5(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(113) |
a6(b3(a1(a4(b6(b3(a1(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(114) |
a6(b3(a1(a4(b2(b5(a6(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(115) |
a6(b3(a1(a4(b2(b5(a2(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(116) |
a6(b3(a1(a4(b2(b1(a4(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(117) |
a6(b3(a1(a4(b2(b1(a0(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(118) |
a4(b2(b1(a4(b6(b7(a7(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(119) |
a4(b2(b1(a4(b6(b7(a3(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(120) |
a4(b2(b1(a4(b6(b3(a5(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(121) |
a4(b2(b1(a4(b6(b3(a1(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(122) |
a4(b2(b1(a4(b2(b5(a6(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(123) |
a4(b2(b1(a4(b2(b5(a2(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(124) |
a4(b2(b1(a4(b2(b1(a4(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(125) |
a4(b2(b1(a4(b2(b1(a0(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(126) |
b7(a3(a1(a4(b6(b7(a7(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(127) |
b7(a3(a1(a4(b6(b7(a3(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(128) |
b7(a3(a1(a4(b6(b3(a5(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(129) |
b7(a3(a1(a4(b6(b3(a1(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(130) |
b7(a3(a1(a4(b2(b5(a6(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(131) |
b7(a3(a1(a4(b2(b5(a2(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(132) |
b7(a3(a1(a4(b2(b1(a4(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(133) |
b7(a3(a1(a4(b2(b1(a0(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(134) |
b5(a2(b1(a4(b6(b7(a7(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(135) |
b5(a2(b1(a4(b6(b7(a3(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(136) |
b5(a2(b1(a4(b6(b3(a5(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(137) |
b5(a2(b1(a4(b6(b3(a1(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(138) |
b5(a2(b1(a4(b2(b5(a6(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(139) |
b5(a2(b1(a4(b2(b5(a2(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(140) |
b5(a2(b1(a4(b2(b1(a4(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(141) |
b5(a2(b1(a4(b2(b1(a0(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(142) |
b6(b3(a1(a4(b6(b7(a7(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(143) |
b6(b3(a1(a4(b6(b7(a3(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(144) |
b6(b3(a1(a4(b6(b3(a5(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(145) |
b6(b3(a1(a4(b6(b3(a1(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(146) |
b6(b3(a1(a4(b2(b5(a6(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(147) |
b6(b3(a1(a4(b2(b5(a2(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(148) |
b6(b3(a1(a4(b2(b1(a4(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(149) |
b6(b3(a1(a4(b2(b1(a0(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(150) |
b4(b2(b1(a4(b6(b7(a7(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(151) |
b4(b2(b1(a4(b6(b7(a3(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(152) |
b4(b2(b1(a4(b6(b3(a5(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(153) |
b4(b2(b1(a4(b6(b3(a1(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(154) |
b4(b2(b1(a4(b2(b5(a6(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(155) |
b4(b2(b1(a4(b2(b5(a2(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(156) |
b4(b2(b1(a4(b2(b1(a4(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(157) |
b4(b2(b1(a4(b2(b1(a0(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(158) |
a7(a3(a1(a4(b6(b7(a7(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(95) |
a7(a3(a1(a4(b6(b7(a3(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(96) |
a7(a3(a1(a4(b6(b3(a5(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(97) |
a7(a3(a1(a4(b6(b3(a1(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(98) |
a7(a3(a1(a4(b2(b5(a6(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(99) |
a7(a3(a1(a4(b2(b5(a2(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(100) |
a7(a3(a1(a4(b2(b1(a4(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(101) |
a7(a3(a1(a4(b2(b1(a0(x1))))))) |
→ |
a7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(102) |
a5(a2(b1(a4(b6(b7(a7(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(103) |
a5(a2(b1(a4(b6(b7(a3(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(104) |
a5(a2(b1(a4(b6(b3(a5(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(105) |
a5(a2(b1(a4(b6(b3(a1(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(106) |
a5(a2(b1(a4(b2(b5(a6(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(107) |
a5(a2(b1(a4(b2(b5(a2(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(108) |
a5(a2(b1(a4(b2(b1(a4(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(109) |
a5(a2(b1(a4(b2(b1(a0(x1))))))) |
→ |
a5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(110) |
a6(b3(a1(a4(b6(b7(a7(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(111) |
a6(b3(a1(a4(b6(b7(a3(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(112) |
a6(b3(a1(a4(b6(b3(a5(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(113) |
a6(b3(a1(a4(b6(b3(a1(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(114) |
a6(b3(a1(a4(b2(b5(a6(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(115) |
a6(b3(a1(a4(b2(b5(a2(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(116) |
a6(b3(a1(a4(b2(b1(a4(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(117) |
a6(b3(a1(a4(b2(b1(a0(x1))))))) |
→ |
a6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(118) |
a4(b2(b1(a4(b6(b7(a7(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(119) |
a4(b2(b1(a4(b6(b7(a3(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(120) |
a4(b2(b1(a4(b6(b3(a1(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(122) |
a4(b2(b1(a4(b2(b5(a6(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(123) |
a4(b2(b1(a4(b2(b5(a2(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(124) |
a4(b2(b1(a4(b2(b1(a4(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(125) |
a4(b2(b1(a4(b2(b1(a0(x1))))))) |
→ |
a4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(126) |
b7(a3(a1(a4(b6(b7(a7(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(127) |
b7(a3(a1(a4(b6(b7(a3(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(128) |
b7(a3(a1(a4(b6(b3(a5(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(129) |
b7(a3(a1(a4(b6(b3(a1(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(130) |
b7(a3(a1(a4(b2(b5(a6(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(131) |
b7(a3(a1(a4(b2(b5(a2(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(132) |
b7(a3(a1(a4(b2(b1(a4(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(133) |
b7(a3(a1(a4(b2(b1(a0(x1))))))) |
→ |
b7(a7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(134) |
b5(a2(b1(a4(b6(b7(a7(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(135) |
b5(a2(b1(a4(b6(b7(a3(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(136) |
b5(a2(b1(a4(b6(b3(a5(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(137) |
b5(a2(b1(a4(b6(b3(a1(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(138) |
b5(a2(b1(a4(b2(b5(a6(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(139) |
b5(a2(b1(a4(b2(b5(a2(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(140) |
b5(a2(b1(a4(b2(b1(a4(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(141) |
b5(a2(b1(a4(b2(b1(a0(x1))))))) |
→ |
b5(a6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(142) |
b6(b3(a1(a4(b6(b7(a7(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(143) |
b6(b3(a1(a4(b6(b7(a3(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(144) |
b6(b3(a1(a4(b6(b3(a5(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a4(b2(b5(x1))))))))) |
(145) |
b6(b3(a1(a4(b6(b3(a1(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(146) |
b6(b3(a1(a4(b2(b5(a6(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(147) |
b6(b3(a1(a4(b2(b5(a2(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(148) |
b6(b3(a1(a4(b2(b1(a4(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(149) |
b6(b3(a1(a4(b2(b1(a0(x1))))))) |
→ |
b6(b7(a3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(150) |
b4(b2(b1(a4(b6(b7(a7(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a4(b6(b7(x1))))))))) |
(151) |
b4(b2(b1(a4(b6(b7(a3(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a4(b6(b3(x1))))))))) |
(152) |
b4(b2(b1(a4(b6(b3(a1(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a4(b2(b1(x1))))))))) |
(154) |
b4(b2(b1(a4(b2(b5(a6(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a0(b4(b6(x1))))))))) |
(155) |
b4(b2(b1(a4(b2(b5(a2(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a0(b4(b2(x1))))))))) |
(156) |
b4(b2(b1(a4(b2(b1(a4(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a0(b0(b4(x1))))))))) |
(157) |
b4(b2(b1(a4(b2(b1(a0(x1))))))) |
→ |
b4(b6(b3(a5(a2(b1(a0(b0(b0(x1))))))))) |
(158) |
There are no rules.
There are no rules in the TRS. Hence, it is terminating.