Termination proof of Relative_05

Termination of the given RelTRS could be proven:

0 RelTRS

↳1 RelTRStoRelADPProof (⇔, 0 ms)

↳2 RelADPP

↳3 RelADPDepGraphProof (⇔, 0 ms)

↳4 AND

    ↳5 RelADPP

        ↳6 RelADPRuleRemovalProof (⇔, 8 ms)

        ↳7 RelADPP

        ↳8 RelADPRuleRemovalProof (⇔, 2 ms)

        ↳9 RelADPP

        ↳10 DAbsisEmptyProof (⇔, 0 ms)

        ↳11 YES

    ↳12 RelADPP

        ↳13 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳14 RelADPP

        ↳15 DAbsisEmptyProof (⇔, 0 ms)

        ↳16 YES

    ↳17 RelADPP

        ↳18 RelADPRuleRemovalProof (⇔, 11 ms)

        ↳19 RelADPP

        ↳20 DAbsisEmptyProof (⇔, 0 ms)

        ↳21 YES

    ↳22 RelADPP

        ↳23 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳24 RelADPP

        ↳25 DAbsisEmptyProof (⇔, 0 ms)

        ↳26 YES

    ↳27 RelADPP

        ↳28 RelADPReductionPairProof (⇔, 45 ms)

        ↳29 RelADPP

        ↳30 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳31 RelADPP

        ↳32 DAbsisEmptyProof (⇔, 0 ms)

        ↳33 YES

    ↳34 RelADPP

        ↳35 RelADPReductionPairProof (⇔, 61 ms)

        ↳36 RelADPP

        ↳37 RelADPReductionPairProof (⇔, 0 ms)

        ↳38 RelADPP

        ↳39 DAbsisEmptyProof (⇔, 0 ms)

        ↳40 YES

    ↳41 RelADPP

        ↳42 RelADPReductionPairProof (⇔, 54 ms)

        ↳43 RelADPP

        ↳44 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳45 RelADPP

        ↳46 DAbsisEmptyProof (⇔, 0 ms)

        ↳47 YES

    ↳48 RelADPP

        ↳49 RelADPReductionPairProof (⇔, 73 ms)

        ↳50 RelADPP

        ↳51 RelADPReductionPairProof (⇔, 3 ms)

        ↳52 RelADPP

        ↳53 RelADPCleverAfsProof (⇒, 0 ms)

        ↳54 QDP

        ↳55 MRRProof (⇔, 0 ms)

        ↳56 QDP

        ↳57 MRRProof (⇔, 0 ms)

        ↳58 QDP

        ↳59 PisEmptyProof (⇔, 0 ms)

        ↳60 YES

    ↳61 RelADPP

        ↳62 RelADPReductionPairProof (⇔, 42 ms)

        ↳63 RelADPP

        ↳64 RelADPReductionPairProof (⇔, 9 ms)

        ↳65 RelADPP

        ↳66 RelADPCleverAfsProof (⇒, 7 ms)

        ↳67 QDP

        ↳68 MRRProof (⇔, 0 ms)

        ↳69 QDP

        ↳70 MRRProof (⇔, 0 ms)

        ↳71 QDP

        ↳72 PisEmptyProof (⇔, 0 ms)

        ↳73 YES

    ↳74 RelADPP

        ↳75 RelADPReductionPairProof (⇔, 54 ms)

        ↳76 RelADPP

        ↳77 RelADPReductionPairProof (⇔, 12 ms)

        ↳78 RelADPP

        ↳79 RelADPCleverAfsProof (⇒, 7 ms)

        ↳80 QDP

        ↳81 MRRProof (⇔, 0 ms)

        ↳82 QDP

        ↳83 MRRProof (⇔, 0 ms)

        ↳84 QDP

        ↳85 PisEmptyProof (⇔, 0 ms)

        ↳86 YES

    ↳87 RelADPP

        ↳88 RelADPReductionPairProof (⇔, 56 ms)

        ↳89 RelADPP

        ↳90 RelADPRuleRemovalProof (⇔, 7 ms)

        ↳91 RelADPP

        ↳92 DAbsisEmptyProof (⇔, 0 ms)

        ↳93 YES

    ↳94 RelADPP

        ↳95 RelADPReductionPairProof (⇔, 45 ms)

        ↳96 RelADPP

        ↳97 RelADPRuleRemovalProof (⇔, 6 ms)

        ↳98 RelADPP

        ↳99 DAbsisEmptyProof (⇔, 0 ms)

        ↳100 YES

    ↳101 RelADPP

        ↳102 RelADPReductionPairProof (⇔, 56 ms)

        ↳103 RelADPP

        ↳104 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳105 RelADPP

        ↳106 DAbsisEmptyProof (⇔, 0 ms)

        ↳107 YES

    ↳108 RelADPP

        ↳109 RelADPReductionPairProof (⇔, 53 ms)

        ↳110 RelADPP

        ↳111 RelADPRuleRemovalProof (⇔, 4 ms)

        ↳112 RelADPP

        ↳113 DAbsisEmptyProof (⇔, 0 ms)

        ↳114 YES

    ↳115 RelADPP

        ↳116 RelADPReductionPairProof (⇔, 49 ms)

        ↳117 RelADPP

        ↳118 RelADPReductionPairProof (⇔, 12 ms)

        ↳119 RelADPP

        ↳120 RelADPDepGraphProof (⇔, 0 ms)

        ↳121 TRUE

    ↳122 RelADPP

        ↳123 RelADPReductionPairProof (⇔, 40 ms)

        ↳124 RelADPP

        ↳125 RelADPRuleRemovalProof (⇔, 3 ms)

        ↳126 RelADPP

        ↳127 DAbsisEmptyProof (⇔, 0 ms)

        ↳128 YES

    ↳129 RelADPP

        ↳130 RelADPReductionPairProof (⇔, 45 ms)

        ↳131 RelADPP

        ↳132 RelADPCleverAfsProof (⇒, 5 ms)

        ↳133 QDP

        ↳134 MRRProof (⇔, 15 ms)

        ↳135 QDP

        ↳136 MRRProof (⇔, 0 ms)

        ↳137 QDP

        ↳138 PisEmptyProof (⇔, 0 ms)

        ↳139 YES

    ↳140 RelADPP

        ↳141 RelADPReductionPairProof (⇔, 48 ms)

        ↳142 RelADPP

        ↳143 RelADPDepGraphProof (⇔, 0 ms)

        ↳144 TRUE

    ↳145 RelADPP

        ↳146 RelADPReductionPairProof (⇔, 58 ms)

        ↳147 RelADPP

        ↳148 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳149 RelADPP

        ↳150 DAbsisEmptyProof (⇔, 0 ms)

        ↳151 YES

    ↳152 RelADPP

        ↳153 RelADPReductionPairProof (⇔, 51 ms)

        ↳154 RelADPP

        ↳155 RelADPReductionPairProof (⇔, 0 ms)

        ↳156 RelADPP

        ↳157 DAbsisEmptyProof (⇔, 0 ms)

        ↳158 YES

    ↳159 RelADPP

        ↳160 RelADPReductionPairProof (⇔, 38 ms)

        ↳161 RelADPP

        ↳162 RelADPRuleRemovalProof (⇔, 6 ms)

        ↳163 RelADPP

        ↳164 DAbsisEmptyProof (⇔, 0 ms)

        ↳165 YES

    ↳166 RelADPP

        ↳167 RelADPReductionPairProof (⇔, 51 ms)

        ↳168 RelADPP

        ↳169 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳170 RelADPP

        ↳171 DAbsisEmptyProof (⇔, 0 ms)

        ↳172 YES

    ↳173 RelADPP

        ↳174 RelADPReductionPairProof (⇔, 37 ms)

        ↳175 RelADPP

        ↳176 RelADPReductionPairProof (⇔, 6 ms)

        ↳177 RelADPP

        ↳178 DAbsisEmptyProof (⇔, 0 ms)

        ↳179 YES

    ↳180 RelADPP

        ↳181 RelADPReductionPairProof (⇔, 56 ms)

        ↳182 RelADPP

        ↳183 RelADPRuleRemovalProof (⇔, 6 ms)

        ↳184 RelADPP

        ↳185 DAbsisEmptyProof (⇔, 0 ms)

        ↳186 YES

    ↳187 RelADPP

        ↳188 RelADPReductionPairProof (⇔, 48 ms)

        ↳189 RelADPP

        ↳190 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳191 RelADPP

        ↳192 DAbsisEmptyProof (⇔, 0 ms)

        ↳193 YES

    ↳194 RelADPP

        ↳195 RelADPReductionPairProof (⇔, 33 ms)

        ↳196 RelADPP

        ↳197 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳198 RelADPP

        ↳199 DAbsisEmptyProof (⇔, 0 ms)

        ↳200 YES

    ↳201 RelADPP

        ↳202 RelADPReductionPairProof (⇔, 31 ms)

        ↳203 RelADPP

        ↳204 RelADPReductionPairProof (⇔, 8 ms)

        ↳205 RelADPP

        ↳206 DAbsisEmptyProof (⇔, 0 ms)

        ↳207 YES

    ↳208 RelADPP

        ↳209 RelADPReductionPairProof (⇔, 41 ms)

        ↳210 RelADPP

        ↳211 RelADPReductionPairProof (⇔, 11 ms)

        ↳212 RelADPP

        ↳213 RelADPCleverAfsProof (⇒, 5 ms)

        ↳214 QDP

        ↳215 MRRProof (⇔, 0 ms)

        ↳216 QDP

        ↳217 MRRProof (⇔, 0 ms)

        ↳218 QDP

        ↳219 PisEmptyProof (⇔, 0 ms)

        ↳220 YES

    ↳221 RelADPP

        ↳222 RelADPReductionPairProof (⇔, 38 ms)

        ↳223 RelADPP

        ↳224 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳225 RelADPP

        ↳226 DAbsisEmptyProof (⇔, 0 ms)

        ↳227 YES

    ↳228 RelADPP

        ↳229 RelADPReductionPairProof (⇔, 45 ms)

        ↳230 RelADPP

        ↳231 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳232 RelADPP

        ↳233 DAbsisEmptyProof (⇔, 0 ms)

        ↳234 YES

    ↳235 RelADPP

        ↳236 RelADPReductionPairProof (⇔, 75 ms)

        ↳237 RelADPP

        ↳238 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳239 RelADPP

        ↳240 DAbsisEmptyProof (⇔, 0 ms)

        ↳241 YES

    ↳242 RelADPP

        ↳243 RelADPReductionPairProof (⇔, 45 ms)

        ↳244 RelADPP

        ↳245 RelADPRuleRemovalProof (⇔, 11 ms)

        ↳246 RelADPP

        ↳247 DAbsisEmptyProof (⇔, 0 ms)

        ↳248 YES

    ↳249 RelADPP

        ↳250 RelADPReductionPairProof (⇔, 72 ms)

        ↳251 RelADPP

        ↳252 RelADPReductionPairProof (⇔, 8 ms)

        ↳253 RelADPP

        ↳254 DAbsisEmptyProof (⇔, 0 ms)

        ↳255 YES

    ↳256 RelADPP

        ↳257 RelADPReductionPairProof (⇔, 43 ms)

        ↳258 RelADPP

        ↳259 RelADPRuleRemovalProof (⇔, 8 ms)

        ↳260 RelADPP

        ↳261 DAbsisEmptyProof (⇔, 0 ms)

        ↳262 YES

    ↳263 RelADPP

        ↳264 RelADPReductionPairProof (⇔, 34 ms)

        ↳265 RelADPP

        ↳266 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳267 RelADPP

        ↳268 DAbsisEmptyProof (⇔, 0 ms)

        ↳269 YES

    ↳270 RelADPP

        ↳271 RelADPReductionPairProof (⇔, 61 ms)

        ↳272 RelADPP

        ↳273 RelADPRuleRemovalProof (⇔, 0 ms)

        ↳274 RelADPP

        ↳275 DAbsisEmptyProof (⇔, 0 ms)

        ↳276 YES

(0) Obligation:

Relative term rewrite system:
The relative TRS consists of the following R rules:

s(a(x)) → s(b(x))
b(b(x)) → a(x)

The relative TRS consists of the following S rules:

f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))

(1) RelTRStoRelADPProof (EQUIVALENT transformation)

We upgrade the RelTRS problem to an equivalent Relative ADP Problem [IJCAR24].

(2) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))
s(a(x)) → s(B(x))
b(b(x)) → A(x)

and relative ADPs:

f(s(x), y) → F(x, S(y))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
s(a(x)) → A(S(x))
a(s(x)) → S(A(x))

(3) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
1 SCC with nodes from P_abs,
35 Lassos,
Result: This relative DT problem is equivalent to 36 subproblems.

(4) Complex Obligation (AND)

(5) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))
b(b(x)) → A(x)
s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))

(6) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))
s(a(x)) → S(b(x))

b(b(x)) → A(x)

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 1 + x₁
POL(f(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(7) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))

(8) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

b(b(x)) → A(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 1 + x₁
POL(b(x₁)) = 3 + x₁
POL(f(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(9) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))

(10) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(11) YES

(12) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
b(b(x)) → a(x)

(13) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(14) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

(15) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(16) YES

(17) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))

(18) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

b(b(x)) → A(x)

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(19) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

(20) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(21) YES

(22) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
b(b(x)) → a(x)

(23) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → S(b(x))

s(a(x)) → s(b(x))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 1 + x₁
POL(f(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(24) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
b(b(x)) → a(x)

(25) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(26) YES

(27) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(28) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(29) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(30) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(31) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))

(32) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(33) YES

(34) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(35) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2 + x₁ + 2·x₁²
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(36) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(37) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(b(x)) → B(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

No rules with annotations remain.
Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2 + x₁²
POL(B(x₁)) = 1 + x₁
POL(F(x₁, x₂)) = 2·x₂
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(38) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(39) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(40) YES

(41) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(42) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(43) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
b(b(x)) → a(x)

(44) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(45) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))

(46) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(47) YES

(48) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(49) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(50) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(51) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:
none

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 1 + x₁
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₂
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(52) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(53) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

Furthermore, We use an argument filter [LPAR04].
Filtering:s_1 = a_1 = b_1 = S_1 = f_2 = 0, 1
Found this filtering by looking at the following order that orders at least one DP strictly:Polynomial interpretation [POLO]:

POL(S(x₁)) = x₁
POL(a(x₁)) = 2 + 2·x₁
POL(b(x₁)) = 1 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = x₁

(54) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))
b0(b0(x)) → a0(x)

Q is empty.
We have to consider all (P,Q,R)-chains.

(55) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

b0(b0(x)) → a0(x)

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 2 + 2·x₁
POL(b0(x₁)) = 2 + 2·x₁
POL(f) = 0
POL(s0(x₁)) = 2 + 2·x₁

(56) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(57) MRRProof (EQUIVALENT transformation)

S0(a0(x)) → S0(b0(x))

Strictly oriented rules of the TRS R:

s0(a0(x)) → s0(b0(x))

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 1 + 2·x₁
POL(b0(x₁)) = x₁
POL(f) = 0
POL(s0(x₁)) = 1 + 2·x₁

(58) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(59) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(60) YES

(61) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(62) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(63) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(64) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(b(x)) → B(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:
none

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2
POL(B(x₁)) = 1 + x₁
POL(F(x₁, x₂)) = 2 + 2·x₂
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(65) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(66) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

POL(S(x₁)) = x₁
POL(a(x₁)) = 2 + 2·x₁
POL(b(x₁)) = 1 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = x₁

(67) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))
b0(b0(x)) → a0(x)

Q is empty.
We have to consider all (P,Q,R)-chains.

(68) MRRProof (EQUIVALENT transformation)

b0(b0(x)) → a0(x)

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 2 + 2·x₁
POL(b0(x₁)) = 2 + 2·x₁
POL(f) = 0
POL(s0(x₁)) = 2 + 2·x₁

(69) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(70) MRRProof (EQUIVALENT transformation)

S0(a0(x)) → S0(b0(x))

Strictly oriented rules of the TRS R:

s0(a0(x)) → s0(b0(x))

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 1 + 2·x₁
POL(b0(x₁)) = x₁
POL(f) = 0
POL(s0(x₁)) = 1 + 2·x₁

(71) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(72) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(73) YES

(74) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(75) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(76) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(77) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:
none

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 1 + x₁
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₂
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(78) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(79) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

POL(S(x₁)) = x₁
POL(a(x₁)) = 2 + 2·x₁
POL(b(x₁)) = 1 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = x₁

(80) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))
b0(b0(x)) → a0(x)

Q is empty.
We have to consider all (P,Q,R)-chains.

(81) MRRProof (EQUIVALENT transformation)

b0(b0(x)) → a0(x)

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 2 + 2·x₁
POL(b0(x₁)) = 2 + 2·x₁
POL(f) = 0
POL(s0(x₁)) = 2 + 2·x₁

(82) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(83) MRRProof (EQUIVALENT transformation)

S0(a0(x)) → S0(b0(x))

Strictly oriented rules of the TRS R:

s0(a0(x)) → s0(b0(x))

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 1 + 2·x₁
POL(b0(x₁)) = x₁
POL(f) = 0
POL(s0(x₁)) = 1 + 2·x₁

(84) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(85) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(86) YES

(87) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(88) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(89) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
b(b(x)) → a(x)

(90) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(91) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))

(92) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(93) YES

(94) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(95) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(96) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(97) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → S(b(x))

s(a(x)) → s(b(x))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 1 + x₁
POL(f(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(98) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(99) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(100) YES

(101) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(102) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁²
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(103) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(104) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → S(b(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(105) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))

(106) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(107) YES

(108) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(109) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(110) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
b(b(x)) → a(x)

(111) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(112) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

(113) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(114) YES

(115) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))

(116) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))

The remaining rules can at least be oriented weakly:
Absolute ADPs:

b(b(x)) → A(x)

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(117) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))

(118) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))

The remaining rules can at least be oriented weakly:
Absolute ADPs:

b(b(x)) → A(x)

Relative ADPs:
none

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2 + 2·x₂
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(119) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))

(120) RelADPDepGraphProof (EQUIVALENT transformation)

We use the relative dependency graph processor [IJCAR24].
The approximation of the Relative Dependency Graph contains:
0 SCCs with nodes from P_abs,
0 Lassos,
Result: This relative DT problem is equivalent to 0 subproblems.

(121) TRUE

(122) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(123) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 2
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(124) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
b(b(x)) → a(x)

(125) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → S(b(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(126) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))

(127) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(128) YES

(129) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(130) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:
none

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 3·x₁²
POL(B(x₁)) = 2
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(131) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(132) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

POL(S(x₁)) = x₁
POL(a(x₁)) = 2 + 2·x₁
POL(b(x₁)) = 1 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = x₁

(133) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))
b0(b0(x)) → a0(x)

Q is empty.
We have to consider all (P,Q,R)-chains.

(134) MRRProof (EQUIVALENT transformation)

b0(b0(x)) → a0(x)

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 2 + 2·x₁
POL(b0(x₁)) = 2 + 2·x₁
POL(f) = 0
POL(s0(x₁)) = 2 + 2·x₁

(135) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(136) MRRProof (EQUIVALENT transformation)

S0(a0(x)) → S0(b0(x))

Strictly oriented rules of the TRS R:

s0(a0(x)) → s0(b0(x))

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 1 + 2·x₁
POL(b0(x₁)) = x₁
POL(f) = 0
POL(s0(x₁)) = 1 + 2·x₁

(137) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(138) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(139) YES

(140) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(141) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:
none

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(142) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(143) RelADPDepGraphProof (EQUIVALENT transformation)

(144) TRUE

(145) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(146) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(147) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
b(b(x)) → a(x)

(148) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → S(b(x))

s(a(x)) → s(b(x))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 1 + x₁
POL(f(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(149) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
b(b(x)) → a(x)

(150) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(151) YES

(152) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(153) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(154) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(155) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

No rules with annotations remain.
Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 1 + x₁
POL(B(x₁)) = 1 + x₁
POL(F(x₁, x₂)) = x₁·x₂ + 2·x₂
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(156) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(157) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(158) YES

(159) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
f(s(x), y) → F(x, S(y))

(160) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
f(s(x), y) → F(x, S(y))

The remaining rules can at least be oriented weakly:
Absolute ADPs:

b(b(x)) → A(x)

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 3·x₁
POL(s(x₁)) = 3 + 2·x₁

(161) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))

(162) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

b(b(x)) → A(x)

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(163) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))

(164) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(165) YES

(166) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))

(167) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))

The remaining rules can at least be oriented weakly:
Absolute ADPs:

b(b(x)) → A(x)

Relative ADPs:

s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(168) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))

(169) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

b(b(x)) → A(x)

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(170) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))

(171) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(172) YES

(173) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))

(174) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))

The remaining rules can at least be oriented weakly:
Absolute ADPs:

b(b(x)) → A(x)

Relative ADPs:

s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(175) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))

(176) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:

b(b(x)) → A(x)

Relative ADPs:

s(b(x)) → B(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))

No rules with annotations remain.
Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2 + 2·x₁
POL(B(x₁)) = 1 + x₁
POL(F(x₁, x₂)) = 0
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(177) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(178) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(179) YES

(180) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(181) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(182) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(183) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(184) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))

(185) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(186) YES

(187) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))

(188) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))

The remaining rules can at least be oriented weakly:
Absolute ADPs:

b(b(x)) → A(x)

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(189) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))

(190) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

b(b(x)) → A(x)

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(191) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))

(192) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(193) YES

(194) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(195) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(196) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(197) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(198) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))

(199) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(200) YES

(201) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(202) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(203) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(204) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

No rules with annotations remain.
Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 1 + x₁
POL(B(x₁)) = 3 + 2·x₁
POL(F(x₁, x₂)) = 2·x₂
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(205) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(206) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(207) YES

(208) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(209) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 3 + x₁
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(210) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(211) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:
none

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 1 + x₁
POL(B(x₁)) = 2
POL(F(x₁, x₂)) = 2 + 2·x₁·x₂ + 2·x₂
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(212) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(213) RelADPCleverAfsProof (SOUND transformation)

We use the first derelatifying processor [IJCAR24].
There are no annotations in relative ADPs, so the relative ADP problem can be transformed into a non-relative DP problem.

POL(S(x₁)) = x₁
POL(a(x₁)) = 2 + 2·x₁
POL(b(x₁)) = 1 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = x₁

(214) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))
b0(b0(x)) → a0(x)

Q is empty.
We have to consider all (P,Q,R)-chains.

(215) MRRProof (EQUIVALENT transformation)

b0(b0(x)) → a0(x)

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 2 + 2·x₁
POL(b0(x₁)) = 2 + 2·x₁
POL(f) = 0
POL(s0(x₁)) = 2 + 2·x₁

(216) Obligation:

Q DP problem:
The TRS P consists of the following rules:

S0(a0(x)) → S0(b0(x))

The TRS R consists of the following rules:

s0(a0(x)) → s0(b0(x))
f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(217) MRRProof (EQUIVALENT transformation)

S0(a0(x)) → S0(b0(x))

Strictly oriented rules of the TRS R:

s0(a0(x)) → s0(b0(x))

Used ordering: Polynomial interpretation [POLO]:

POL(S0(x₁)) = x₁
POL(a0(x₁)) = 1 + 2·x₁
POL(b0(x₁)) = x₁
POL(f) = 0
POL(s0(x₁)) = 1 + 2·x₁

(218) Obligation:

Q DP problem:
P is empty.
The TRS R consists of the following rules:

f → f
s0(b0(x)) → b0(s0(x))
b0(s0(x)) → s0(b0(x))
s0(a0(x)) → a0(s0(x))
a0(s0(x)) → s0(a0(x))

Q is empty.
We have to consider all (P,Q,R)-chains.

(219) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(220) YES

(221) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(222) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(223) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
b(b(x)) → a(x)

(224) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(225) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

(226) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(227) YES

(228) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(229) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(230) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
b(b(x)) → a(x)

(231) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → S(b(x))

s(a(x)) → s(b(x))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 1 + x₁
POL(f(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(232) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
b(b(x)) → a(x)

(233) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(234) YES

(235) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
f(s(x), y) → F(x, S(y))

(236) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → F(x, S(y))

The remaining rules can at least be oriented weakly:
Absolute ADPs:

b(b(x)) → A(x)

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(237) Obligation:

Relative ADP Problem with
absolute ADPs:

b(b(x)) → A(x)

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))

(238) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

b(b(x)) → A(x)

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(239) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

(240) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(241) YES

(242) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(243) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(244) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(245) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → S(b(x))

s(a(x)) → s(b(x))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 1 + x₁
POL(f(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(246) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(247) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(248) YES

(249) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(250) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(251) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(252) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
s(b(x)) → B(S(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → s(b(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

No rules with annotations remain.
Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 1 + x₁
POL(B(x₁)) = 1 + x₁
POL(F(x₁, x₂)) = x₁·x₂ + 2·x₂
POL(S(x₁)) = 2 + 2·x₁
POL(a(x₁)) = 3 + 2·x₁
POL(b(x₁)) = 3 + 2·x₁
POL(f(x₁, x₂)) = 0
POL(s(x₁)) = 3 + 2·x₁

(253) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
s(a(x)) → a(s(x))
a(s(x)) → s(a(x))
b(b(x)) → a(x)

(254) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(255) YES

(256) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(257) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → s(B(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = x₁
POL(s(x₁)) = 3 + 2·x₁

(258) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → s(B(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))
b(b(x)) → a(x)

(259) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → s(B(x))

s(a(x)) → s(b(x))
f(s(x), y) → f(x, s(y))
b(b(x)) → a(x)

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 3 + x₁
POL(b(x₁)) = 2 + x₁
POL(f(x₁, x₂)) = 3·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(260) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → b(s(x))
b(s(x)) → s(b(x))

(261) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(262) YES

(263) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(264) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(265) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
b(b(x)) → a(x)

(266) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → S(b(x))

s(a(x)) → s(b(x))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 1 + x₁
POL(f(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(267) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
b(b(x)) → a(x)

(268) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.

(269) YES

(270) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))
b(b(x)) → a(x)
f(s(x), y) → F(x, S(y))

(271) RelADPReductionPairProof (EQUIVALENT transformation)

We use the reduction pair processor [IJCAR24].
The following rules can be oriented strictly (l^# > ann(r))
and therefore we can remove all of its annotations in the right-hand side:
Relative ADPs:

s(a(x)) → s(b(x))
f(s(x), y) → F(x, S(y))
b(b(x)) → a(x)

The remaining rules can at least be oriented weakly:
Absolute ADPs:

s(a(x)) → S(b(x))

Relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
b(s(x)) → S(B(x))

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 0
POL(B(x₁)) = 0
POL(F(x₁, x₂)) = 2·x₁
POL(S(x₁)) = 0
POL(a(x₁)) = x₁
POL(b(x₁)) = x₁
POL(f(x₁, x₂)) = 2·x₁
POL(s(x₁)) = 3 + 2·x₁

(272) Obligation:

Relative ADP Problem with
absolute ADPs:

s(a(x)) → S(b(x))

and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(a(x)) → s(b(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
b(b(x)) → a(x)

(273) RelADPRuleRemovalProof (EQUIVALENT transformation)

We use the rule removal processor [IJCAR24].
The following rules can be ordered strictly and therefore removed:

s(a(x)) → S(b(x))

s(a(x)) → s(b(x))

c:

Ordered with Polynomial interpretation [POLO]:

POL(A(x₁)) = 2·x₁
POL(B(x₁)) = 2·x₁
POL(S(x₁)) = 2·x₁
POL(a(x₁)) = 2 + x₁
POL(b(x₁)) = 1 + x₁
POL(f(x₁, x₂)) = 2·x₁ + 2·x₂
POL(s(x₁)) = 3 + x₁

(274) Obligation:

Relative ADP Problem with
No absolute ADPs, and relative ADPs:

s(a(x)) → A(S(x))
a(s(x)) → S(A(x))
s(b(x)) → B(S(x))
f(s(x), y) → f(x, s(y))
b(s(x)) → S(B(x))
b(b(x)) → a(x)

(275) DAbsisEmptyProof (EQUIVALENT transformation)

The relative ADP Problem has an empty P_abs. Hence, no infinite chain exists.