Certification Problem
Input (TPDB SRS_Relative/Waldmann_06_relative/rbeans)
The relative rewrite relation R/S is considered where R is the following TRS
|
b(a(a(x1))) |
→ |
a(b(c(x1))) |
(1) |
|
c(a(x1)) |
→ |
a(c(x1)) |
(2) |
|
c(b(x1)) |
→ |
b(a(x1)) |
(3) |
and S is the following TRS.
Property / Task
Prove or disprove termination.Answer / Result
Yes.Proof (by matchbox @ termCOMP 2023)
1 Closure Under Flat Contexts
Using the flat contexts
{c(☐), b(☐), a(☐)}
We obtain the transformed TRS
|
c(b(a(a(x1)))) |
→ |
c(a(b(c(x1)))) |
(5) |
|
c(c(a(x1))) |
→ |
c(a(c(x1))) |
(6) |
|
c(c(b(x1))) |
→ |
c(b(a(x1))) |
(7) |
|
b(b(a(a(x1)))) |
→ |
b(a(b(c(x1)))) |
(8) |
|
b(c(a(x1))) |
→ |
b(a(c(x1))) |
(9) |
|
b(c(b(x1))) |
→ |
b(b(a(x1))) |
(10) |
|
a(b(a(a(x1)))) |
→ |
a(a(b(c(x1)))) |
(11) |
|
a(c(a(x1))) |
→ |
a(a(c(x1))) |
(12) |
|
a(c(b(x1))) |
→ |
a(b(a(x1))) |
(13) |
|
c(x1) |
→ |
c(b(x1)) |
(14) |
|
b(x1) |
→ |
b(b(x1)) |
(15) |
|
a(x1) |
→ |
a(b(x1)) |
(16) |
1.1 Closure Under Flat Contexts
Using the flat contexts
{c(☐), b(☐), a(☐)}
We obtain the transformed TRS
|
c(c(b(a(a(x1))))) |
→ |
c(c(a(b(c(x1))))) |
(17) |
|
c(c(c(a(x1)))) |
→ |
c(c(a(c(x1)))) |
(18) |
|
c(c(c(b(x1)))) |
→ |
c(c(b(a(x1)))) |
(19) |
|
c(b(b(a(a(x1))))) |
→ |
c(b(a(b(c(x1))))) |
(20) |
|
c(b(c(a(x1)))) |
→ |
c(b(a(c(x1)))) |
(21) |
|
c(b(c(b(x1)))) |
→ |
c(b(b(a(x1)))) |
(22) |
|
c(a(b(a(a(x1))))) |
→ |
c(a(a(b(c(x1))))) |
(23) |
|
c(a(c(a(x1)))) |
→ |
c(a(a(c(x1)))) |
(24) |
|
c(a(c(b(x1)))) |
→ |
c(a(b(a(x1)))) |
(25) |
|
b(c(b(a(a(x1))))) |
→ |
b(c(a(b(c(x1))))) |
(26) |
|
b(c(c(a(x1)))) |
→ |
b(c(a(c(x1)))) |
(27) |
|
b(c(c(b(x1)))) |
→ |
b(c(b(a(x1)))) |
(28) |
|
b(b(b(a(a(x1))))) |
→ |
b(b(a(b(c(x1))))) |
(29) |
|
b(b(c(a(x1)))) |
→ |
b(b(a(c(x1)))) |
(30) |
|
b(b(c(b(x1)))) |
→ |
b(b(b(a(x1)))) |
(31) |
|
b(a(b(a(a(x1))))) |
→ |
b(a(a(b(c(x1))))) |
(32) |
|
b(a(c(a(x1)))) |
→ |
b(a(a(c(x1)))) |
(33) |
|
b(a(c(b(x1)))) |
→ |
b(a(b(a(x1)))) |
(34) |
|
a(c(b(a(a(x1))))) |
→ |
a(c(a(b(c(x1))))) |
(35) |
|
a(c(c(a(x1)))) |
→ |
a(c(a(c(x1)))) |
(36) |
|
a(c(c(b(x1)))) |
→ |
a(c(b(a(x1)))) |
(37) |
|
a(b(b(a(a(x1))))) |
→ |
a(b(a(b(c(x1))))) |
(38) |
|
a(b(c(a(x1)))) |
→ |
a(b(a(c(x1)))) |
(39) |
|
a(b(c(b(x1)))) |
→ |
a(b(b(a(x1)))) |
(40) |
|
a(a(b(a(a(x1))))) |
→ |
a(a(a(b(c(x1))))) |
(41) |
|
a(a(c(a(x1)))) |
→ |
a(a(a(c(x1)))) |
(42) |
|
a(a(c(b(x1)))) |
→ |
a(a(b(a(x1)))) |
(43) |
|
c(c(x1)) |
→ |
c(c(b(x1))) |
(44) |
|
c(b(x1)) |
→ |
c(b(b(x1))) |
(45) |
|
c(a(x1)) |
→ |
c(a(b(x1))) |
(46) |
|
b(c(x1)) |
→ |
b(c(b(x1))) |
(47) |
|
b(b(x1)) |
→ |
b(b(b(x1))) |
(48) |
|
b(a(x1)) |
→ |
b(a(b(x1))) |
(49) |
|
a(c(x1)) |
→ |
a(c(b(x1))) |
(50) |
|
a(b(x1)) |
→ |
a(b(b(x1))) |
(51) |
|
a(a(x1)) |
→ |
a(a(b(x1))) |
(52) |
1.1.1 Semantic Labeling
The following interpretations form a
model
of the rules.
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 |
We obtain the labeled TRS
There are 324 ruless (increase limit for explicit display).
1.1.1.1 Rule Removal
Using the
matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
| [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 +
|
all of the following rules can be deleted.
|
b4(b7(b8(a5(a4(x1))))) |
→ |
b7(b5(a1(b3(c4(x1))))) |
(53) |
|
b4(b7(b8(a5(a7(x1))))) |
→ |
b7(b5(a1(b3(c7(x1))))) |
(54) |
|
b4(b7(b8(a5(a1(x1))))) |
→ |
b7(b5(a1(b3(c1(x1))))) |
(55) |
|
b4(b7(b8(a8(a5(x1))))) |
→ |
b7(b5(a1(b6(c5(x1))))) |
(56) |
|
b4(b7(b8(a8(a8(x1))))) |
→ |
b7(b5(a1(b6(c8(x1))))) |
(57) |
|
b4(b7(b8(a8(a2(x1))))) |
→ |
b7(b5(a1(b6(c2(x1))))) |
(58) |
|
b4(b7(b8(a2(a3(x1))))) |
→ |
b7(b5(a1(b0(c3(x1))))) |
(59) |
|
b4(b7(b8(a2(a6(x1))))) |
→ |
b7(b5(a1(b0(c6(x1))))) |
(60) |
|
b4(b7(b8(a2(a0(x1))))) |
→ |
b7(b5(a1(b0(c0(x1))))) |
(61) |
|
b1(b6(c5(a4(x1)))) |
→ |
b7(b2(a3(c4(x1)))) |
(134) |
|
b1(b6(c5(a7(x1)))) |
→ |
b7(b2(a3(c7(x1)))) |
(135) |
|
b1(b6(c5(a1(x1)))) |
→ |
b7(b2(a3(c1(x1)))) |
(136) |
|
b1(b6(c8(a5(x1)))) |
→ |
b7(b2(a6(c5(x1)))) |
(137) |
|
b1(b6(c8(a8(x1)))) |
→ |
b7(b2(a6(c8(x1)))) |
(138) |
|
b1(b6(c8(a2(x1)))) |
→ |
b7(b2(a6(c2(x1)))) |
(139) |
|
b1(b6(c2(a3(x1)))) |
→ |
b7(b2(a0(c3(x1)))) |
(140) |
|
b1(b6(c2(a6(x1)))) |
→ |
b7(b2(a0(c6(x1)))) |
(141) |
|
b1(b6(c2(a0(x1)))) |
→ |
b7(b2(a0(c0(x1)))) |
(142) |
|
b1(b3(c4(b4(x1)))) |
→ |
b4(b7(b5(a4(x1)))) |
(215) |
|
b1(b3(c4(b1(x1)))) |
→ |
b4(b7(b5(a1(x1)))) |
(217) |
|
b2(a3(c4(b4(x1)))) |
→ |
b5(a7(b5(a4(x1)))) |
(224) |
|
b2(a3(c4(b1(x1)))) |
→ |
b5(a7(b5(a1(x1)))) |
(226) |
|
b0(c3(c4(b4(x1)))) |
→ |
b3(c7(b5(a4(x1)))) |
(233) |
|
b0(c3(c4(b1(x1)))) |
→ |
b3(c7(b5(a1(x1)))) |
(235) |
|
a1(b3(c4(b4(x1)))) |
→ |
a4(b7(b5(a4(x1)))) |
(242) |
|
a1(b3(c4(b1(x1)))) |
→ |
a4(b7(b5(a1(x1)))) |
(244) |
|
a2(a3(c4(b4(x1)))) |
→ |
a5(a7(b5(a4(x1)))) |
(251) |
|
a2(a3(c4(b1(x1)))) |
→ |
a5(a7(b5(a1(x1)))) |
(253) |
|
a0(c3(c4(b4(x1)))) |
→ |
a3(c7(b5(a4(x1)))) |
(260) |
|
a0(c3(c4(b1(x1)))) |
→ |
a3(c7(b5(a1(x1)))) |
(262) |
|
c1(b3(c4(b4(x1)))) |
→ |
c4(b7(b5(a4(x1)))) |
(269) |
|
c1(b3(c4(b1(x1)))) |
→ |
c4(b7(b5(a1(x1)))) |
(271) |
|
c2(a3(c4(b4(x1)))) |
→ |
c5(a7(b5(a4(x1)))) |
(278) |
|
c2(a3(c4(b1(x1)))) |
→ |
c5(a7(b5(a1(x1)))) |
(280) |
|
c0(c3(c4(b4(x1)))) |
→ |
c3(c7(b5(a4(x1)))) |
(287) |
|
c0(c3(c4(b1(x1)))) |
→ |
c3(c7(b5(a1(x1)))) |
(289) |
|
b5(a7(x1)) |
→ |
b5(a4(b7(x1))) |
(306) |
|
b8(a5(x1)) |
→ |
b5(a7(b5(x1))) |
(308) |
|
b8(a8(x1)) |
→ |
b5(a7(b8(x1))) |
(309) |
|
b8(a2(x1)) |
→ |
b5(a7(b2(x1))) |
(310) |
|
b2(a3(x1)) |
→ |
b5(a1(b3(x1))) |
(311) |
|
b2(a6(x1)) |
→ |
b5(a1(b6(x1))) |
(312) |
|
b2(a0(x1)) |
→ |
b5(a1(b0(x1))) |
(313) |
|
b3(c7(x1)) |
→ |
b3(c4(b7(x1))) |
(315) |
|
b6(c5(x1)) |
→ |
b3(c7(b5(x1))) |
(317) |
|
b6(c8(x1)) |
→ |
b3(c7(b8(x1))) |
(318) |
|
b6(c2(x1)) |
→ |
b3(c7(b2(x1))) |
(319) |
|
b0(c3(x1)) |
→ |
b3(c1(b3(x1))) |
(320) |
|
b0(c6(x1)) |
→ |
b3(c1(b6(x1))) |
(321) |
|
b0(c0(x1)) |
→ |
b3(c1(b0(x1))) |
(322) |
|
a7(b5(x1)) |
→ |
a4(b7(b5(x1))) |
(326) |
|
a7(b8(x1)) |
→ |
a4(b7(b8(x1))) |
(327) |
|
a7(b2(x1)) |
→ |
a4(b7(b2(x1))) |
(328) |
|
a5(a7(x1)) |
→ |
a5(a4(b7(x1))) |
(333) |
|
a8(a5(x1)) |
→ |
a5(a7(b5(x1))) |
(335) |
|
a8(a8(x1)) |
→ |
a5(a7(b8(x1))) |
(336) |
|
a8(a2(x1)) |
→ |
a5(a7(b2(x1))) |
(337) |
|
a2(a3(x1)) |
→ |
a5(a1(b3(x1))) |
(338) |
|
a2(a6(x1)) |
→ |
a5(a1(b6(x1))) |
(339) |
|
a2(a0(x1)) |
→ |
a5(a1(b0(x1))) |
(340) |
|
a3(c7(x1)) |
→ |
a3(c4(b7(x1))) |
(342) |
|
a6(c5(x1)) |
→ |
a3(c7(b5(x1))) |
(344) |
|
a6(c8(x1)) |
→ |
a3(c7(b8(x1))) |
(345) |
|
a6(c2(x1)) |
→ |
a3(c7(b2(x1))) |
(346) |
|
a0(c3(x1)) |
→ |
a3(c1(b3(x1))) |
(347) |
|
a0(c6(x1)) |
→ |
a3(c1(b6(x1))) |
(348) |
|
a0(c0(x1)) |
→ |
a3(c1(b0(x1))) |
(349) |
|
c7(b5(x1)) |
→ |
c4(b7(b5(x1))) |
(353) |
|
c7(b8(x1)) |
→ |
c4(b7(b8(x1))) |
(354) |
|
c7(b2(x1)) |
→ |
c4(b7(b2(x1))) |
(355) |
|
c5(a7(x1)) |
→ |
c5(a4(b7(x1))) |
(360) |
|
c8(a5(x1)) |
→ |
c5(a7(b5(x1))) |
(362) |
|
c8(a8(x1)) |
→ |
c5(a7(b8(x1))) |
(363) |
|
c8(a2(x1)) |
→ |
c5(a7(b2(x1))) |
(364) |
|
c2(a3(x1)) |
→ |
c5(a1(b3(x1))) |
(365) |
|
c2(a6(x1)) |
→ |
c5(a1(b6(x1))) |
(366) |
|
c2(a0(x1)) |
→ |
c5(a1(b0(x1))) |
(367) |
|
c3(c7(x1)) |
→ |
c3(c4(b7(x1))) |
(369) |
|
c6(c5(x1)) |
→ |
c3(c7(b5(x1))) |
(371) |
|
c6(c8(x1)) |
→ |
c3(c7(b8(x1))) |
(372) |
|
c6(c2(x1)) |
→ |
c3(c7(b2(x1))) |
(373) |
|
c0(c3(x1)) |
→ |
c3(c1(b3(x1))) |
(374) |
|
c0(c6(x1)) |
→ |
c3(c1(b6(x1))) |
(375) |
|
c0(c0(x1)) |
→ |
c3(c1(b0(x1))) |
(376) |
1.1.1.1.1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
There are 240 ruless (increase limit for explicit display).
1.1.1.1.1.1 Rule Removal
Using the
matrix interpretations of dimension 1 with strict dimension 1 over the naturals
| [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 +
|
all of the following rules can be deleted.
There are 152 ruless (increase limit for explicit display).
1.1.1.1.1.1.1 Rule Removal
Using the
matrix interpretations of dimension 1 with strict dimension 1 over the rationals with delta = 1
| [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 +
|
all of the following rules can be deleted.
|
a4(a5(b8(a7(b5(x1))))) |
→ |
c4(b3(a1(a5(b8(x1))))) |
(377) |
|
a1(a5(b8(a7(b5(x1))))) |
→ |
c1(b3(a1(a5(b8(x1))))) |
(379) |
|
a4(a5(b8(c7(b3(x1))))) |
→ |
c4(b3(a1(c5(b6(x1))))) |
(386) |
|
a1(a5(b8(c7(b3(x1))))) |
→ |
c1(b3(a1(c5(b6(x1))))) |
(388) |
|
a4(a5(b8(b7(a4(x1))))) |
→ |
c4(b3(a1(b5(a7(x1))))) |
(395) |
|
a1(a5(b8(b7(a4(x1))))) |
→ |
c1(b3(a1(b5(a7(x1))))) |
(397) |
|
a4(a5(b8(a7(a5(x1))))) |
→ |
c4(b3(a1(a5(a8(x1))))) |
(404) |
|
a1(a5(b8(a7(a5(x1))))) |
→ |
c1(b3(a1(a5(a8(x1))))) |
(406) |
|
a4(a5(b8(c7(a3(x1))))) |
→ |
c4(b3(a1(c5(a6(x1))))) |
(413) |
|
a1(a5(b8(c7(a3(x1))))) |
→ |
c1(b3(a1(c5(a6(x1))))) |
(415) |
|
a4(a5(b8(a7(c5(x1))))) |
→ |
c4(b3(a1(a5(c8(x1))))) |
(431) |
|
a1(a5(b8(a7(c5(x1))))) |
→ |
c1(b3(a1(a5(c8(x1))))) |
(433) |
|
a4(a5(b8(c7(c3(x1))))) |
→ |
c4(b3(a1(c5(c6(x1))))) |
(440) |
|
a1(a5(b8(c7(c3(x1))))) |
→ |
c1(b3(a1(c5(c6(x1))))) |
(442) |
|
a4(c5(a6(b2(x1)))) |
→ |
c4(a3(a2(b8(x1)))) |
(449) |
|
a1(c5(a6(b2(x1)))) |
→ |
c1(a3(a2(b8(x1)))) |
(451) |
|
a4(c5(c6(b0(x1)))) |
→ |
c4(a3(c2(b6(x1)))) |
(458) |
|
a1(c5(c6(b0(x1)))) |
→ |
c1(a3(c2(b6(x1)))) |
(460) |
|
a4(c5(b6(a1(x1)))) |
→ |
c4(a3(b2(a7(x1)))) |
(467) |
|
a1(c5(b6(a1(x1)))) |
→ |
c1(a3(b2(a7(x1)))) |
(469) |
|
a4(c5(a6(a2(x1)))) |
→ |
c4(a3(a2(a8(x1)))) |
(476) |
|
a1(c5(a6(a2(x1)))) |
→ |
c1(a3(a2(a8(x1)))) |
(478) |
|
a4(c5(c6(a0(x1)))) |
→ |
c4(a3(c2(a6(x1)))) |
(485) |
|
a1(c5(c6(a0(x1)))) |
→ |
c1(a3(c2(a6(x1)))) |
(487) |
|
a4(c5(a6(c2(x1)))) |
→ |
c4(a3(a2(c8(x1)))) |
(503) |
|
a1(c5(a6(c2(x1)))) |
→ |
c1(a3(a2(c8(x1)))) |
(505) |
|
a4(c5(c6(c0(x1)))) |
→ |
c4(a3(c2(c6(x1)))) |
(512) |
|
a1(c5(c6(c0(x1)))) |
→ |
c1(a3(c2(c6(x1)))) |
(514) |
|
b5(c7(b3(b1(x1)))) |
→ |
a5(b8(b7(b4(x1)))) |
(522) |
|
b8(c7(b3(b1(x1)))) |
→ |
a8(b8(b7(b4(x1)))) |
(523) |
|
b2(c7(b3(b1(x1)))) |
→ |
a2(b8(b7(b4(x1)))) |
(524) |
|
b5(c7(a3(b2(x1)))) |
→ |
a5(b8(a7(b5(x1)))) |
(529) |
|
b8(c7(a3(b2(x1)))) |
→ |
a8(b8(a7(b5(x1)))) |
(530) |
|
b2(c7(a3(b2(x1)))) |
→ |
a2(b8(a7(b5(x1)))) |
(531) |
|
b5(c7(c3(b0(x1)))) |
→ |
a5(b8(c7(b3(x1)))) |
(536) |
|
b8(c7(c3(b0(x1)))) |
→ |
a8(b8(c7(b3(x1)))) |
(537) |
|
b2(c7(c3(b0(x1)))) |
→ |
a2(b8(c7(b3(x1)))) |
(538) |
|
b5(c7(b3(a1(x1)))) |
→ |
a5(b8(b7(a4(x1)))) |
(543) |
|
b8(c7(b3(a1(x1)))) |
→ |
a8(b8(b7(a4(x1)))) |
(544) |
|
b2(c7(b3(a1(x1)))) |
→ |
a2(b8(b7(a4(x1)))) |
(545) |
|
b5(c7(a3(a2(x1)))) |
→ |
a5(b8(a7(a5(x1)))) |
(550) |
|
b8(c7(a3(a2(x1)))) |
→ |
a8(b8(a7(a5(x1)))) |
(551) |
|
b2(c7(a3(a2(x1)))) |
→ |
a2(b8(a7(a5(x1)))) |
(552) |
|
b5(c7(c3(a0(x1)))) |
→ |
a5(b8(c7(a3(x1)))) |
(557) |
|
b8(c7(c3(a0(x1)))) |
→ |
a8(b8(c7(a3(x1)))) |
(558) |
|
b2(c7(c3(a0(x1)))) |
→ |
a2(b8(c7(a3(x1)))) |
(559) |
|
b5(c7(b3(c1(x1)))) |
→ |
a5(b8(b7(c4(x1)))) |
(564) |
|
b8(c7(b3(c1(x1)))) |
→ |
a8(b8(b7(c4(x1)))) |
(565) |
|
b2(c7(b3(c1(x1)))) |
→ |
a2(b8(b7(c4(x1)))) |
(566) |
|
b5(c7(a3(c2(x1)))) |
→ |
a5(b8(a7(c5(x1)))) |
(571) |
|
b8(c7(a3(c2(x1)))) |
→ |
a8(b8(a7(c5(x1)))) |
(572) |
|
b2(c7(a3(c2(x1)))) |
→ |
a2(b8(a7(c5(x1)))) |
(573) |
|
b5(c7(c3(c0(x1)))) |
→ |
a5(b8(c7(c3(x1)))) |
(578) |
|
b8(c7(c3(c0(x1)))) |
→ |
a8(b8(c7(c3(x1)))) |
(579) |
|
b2(c7(c3(c0(x1)))) |
→ |
a2(b8(c7(c3(x1)))) |
(580) |
|
a1(b5(x1)) |
→ |
b1(a4(b5(x1))) |
(593) |
|
c1(b3(x1)) |
→ |
b1(c4(b3(x1))) |
(595) |
|
b3(a1(x1)) |
→ |
b3(b1(a4(x1))) |
(599) |
|
b6(a1(x1)) |
→ |
b6(b1(a4(x1))) |
(600) |
|
b0(a1(x1)) |
→ |
b0(b1(a4(x1))) |
(601) |
|
a1(a5(x1)) |
→ |
b1(a4(a5(x1))) |
(603) |
|
c1(a3(x1)) |
→ |
b1(c4(a3(x1))) |
(605) |
|
b3(c1(x1)) |
→ |
b3(b1(c4(x1))) |
(609) |
|
b6(c1(x1)) |
→ |
b6(b1(c4(x1))) |
(610) |
|
b0(c1(x1)) |
→ |
b0(b1(c4(x1))) |
(611) |
|
a1(c5(x1)) |
→ |
b1(a4(c5(x1))) |
(613) |
|
c1(c3(x1)) |
→ |
b1(c4(c3(x1))) |
(615) |
1.1.1.1.1.1.1.1 String Reversal
Since only unary symbols occur, one can reverse all terms and obtains the TRS
|
b4(b4(x1)) |
→ |
b4(b4(b4(x1))) |
(296) |
|
b4(b7(x1)) |
→ |
b4(b4(b7(x1))) |
(297) |
|
b4(b1(x1)) |
→ |
b4(b4(b1(x1))) |
(298) |
|
b7(b5(x1)) |
→ |
b4(b7(b5(x1))) |
(299) |
|
b7(b8(x1)) |
→ |
b4(b7(b8(x1))) |
(300) |
|
b7(b2(x1)) |
→ |
b4(b7(b2(x1))) |
(301) |
|
b1(b3(x1)) |
→ |
b4(b1(b3(x1))) |
(302) |
|
b1(b6(x1)) |
→ |
b4(b1(b6(x1))) |
(303) |
|
b1(b0(x1)) |
→ |
b4(b1(b0(x1))) |
(304) |
|
b5(a4(x1)) |
→ |
b5(a4(b4(x1))) |
(305) |
|
b3(c4(x1)) |
→ |
b3(c4(b4(x1))) |
(314) |
|
a4(b4(x1)) |
→ |
a4(b4(b4(x1))) |
(323) |
|
a4(b7(x1)) |
→ |
a4(b4(b7(x1))) |
(324) |
|
a4(b1(x1)) |
→ |
a4(b4(b1(x1))) |
(325) |
|
a5(a4(x1)) |
→ |
a5(a4(b4(x1))) |
(332) |
|
a3(c4(x1)) |
→ |
a3(c4(b4(x1))) |
(341) |
|
c4(b4(x1)) |
→ |
c4(b4(b4(x1))) |
(350) |
|
c4(b7(x1)) |
→ |
c4(b4(b7(x1))) |
(351) |
|
c4(b1(x1)) |
→ |
c4(b4(b1(x1))) |
(352) |
|
c5(a4(x1)) |
→ |
c5(a4(b4(x1))) |
(359) |
|
c3(c4(x1)) |
→ |
c3(c4(b4(x1))) |
(368) |
1.1.1.1.1.1.1.1.1 R is empty
There are no rules in the TRS. Hence, it is terminating.