Termination Proof using AProVE

Term Rewriting System R:
[x]
f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x))))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(b, f(a, f(a, f(a, f(b, x))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(b, f(a, f(a, f(a, f(b, x)))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(b, x))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(b, x)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Modular Removal of Rules

Dependency Pairs:

F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(b, x)))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(a, f(b, x))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> F(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))

Rule:

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

The original DP problem is in applicative form. Its DPs and usable rules are the following.

f(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) -> f(a, f(b, f(a, f(a, f(b, f(a, f(a, f(a, f(b, x)))))))))

It is proper and hence, it can be A-transformed which results in the DP problem

A(a(b(a(a(b(a(x))))))) -> A(a(b(x)))
A(a(b(a(a(b(a(x))))))) -> A(a(a(b(x))))
A(a(b(a(a(b(a(x))))))) -> A(a(b(a(a(a(b(x)))))))

a(a(b(a(a(b(a(x))))))) -> a(b(a(a(b(a(a(a(b(x)))))))))

To remove rules and DPs from this DP problem we used the following monotonic and C_E-compatible order: Polynomial ordering.
Polynomial interpretation:

POL(b(x₁)) = x₁

POL(a(x₁)) = x₁

POL(A(x₁)) = 1 + x₁

We have the following set D of usable symbols: {b, a, A}
No Dependency Pairs can be deleted.
No Rules can be deleted.

The result of this processor delivers one new DP problem.
Note that we keep the A-transformed DP problem as result of this processor.

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Narrowing Transformation

Dependency Pairs:

A(a(b(a(a(b(a(x))))))) -> A(a(b(x)))
A(a(b(a(a(b(a(x))))))) -> A(a(a(b(x))))
A(a(b(a(a(b(a(x))))))) -> A(a(b(a(a(a(b(x)))))))

Rule:

a(a(b(a(a(b(a(x))))))) -> a(b(a(a(b(a(a(a(b(x)))))))))

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(a(b(a(a(b(a(x))))))) -> A(a(a(b(x))))

one new Dependency Pair is created:

A(a(b(a(a(b(a(a(a(b(a(x''))))))))))) -> A(a(b(a(a(b(a(a(a(b(x''))))))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Nar

...

               →DP Problem 3

                 ↳Narrowing Transformation

Dependency Pairs:

A(a(b(a(a(b(a(a(a(b(a(x''))))))))))) -> A(a(b(a(a(b(a(a(a(b(x''))))))))))
A(a(b(a(a(b(a(x))))))) -> A(a(b(a(a(a(b(x)))))))
A(a(b(a(a(b(a(x))))))) -> A(a(b(x)))

Rule:

a(a(b(a(a(b(a(x))))))) -> a(b(a(a(b(a(a(a(b(x)))))))))

On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

A(a(b(a(a(b(a(x))))))) -> A(a(b(a(a(a(b(x)))))))

one new Dependency Pair is created:

A(a(b(a(a(b(a(a(a(b(a(x''))))))))))) -> A(a(b(a(a(b(a(a(b(a(a(a(b(x'')))))))))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳MRR

           →DP Problem 2

             ↳Nar

...

               →DP Problem 4

                 ↳RFC Match Bounds

Dependency Pairs:

A(a(b(a(a(b(a(a(a(b(a(x''))))))))))) -> A(a(b(a(a(b(a(a(b(a(a(a(b(x'')))))))))))))
A(a(b(a(a(b(a(x))))))) -> A(a(b(x)))
A(a(b(a(a(b(a(a(a(b(a(x''))))))))))) -> A(a(b(a(a(b(a(a(a(b(x''))))))))))

Rule:

a(a(b(a(a(b(a(x))))))) -> a(b(a(a(b(a(a(a(b(x)))))))))

Using RFC Match Bounds, the DP problem could be solved. The Match Bound was 2.
The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

202, 203, 204, 205, 206, 207, 208, 209, 210, 211, 212, 213, 214, 215, 216, 217, 218, 219, 220, 221, 222, 223, 224, 225, 226, 227, 228, 229, 230, 231, 232, 233, 234, 235, 236, 237, 238, 239, 240, 241, 242, 243, 244, 245, 246, 247, 248, 249, 250, 251, 252, 253, 254, 255, 256, 257, 258, 259, 260, 261, 262, 263, 264, 265, 266, 267, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 278, 279, 280, 281, 282, 283, 284, 285, 286, 287, 288

Node 202 is start node and node 203 is final node.

Those nodes are connect through the following edges:

203 to 203 labelled #(0)
202 to 204 labelled A(0)
204 to 205 labelled a(0)
205 to 206 labelled b(0)
206 to 207 labelled a(0)
207 to 208 labelled a(0)
208 to 209 labelled b(0)
209 to 210 labelled a(0)
210 to 211 labelled a(0)
211 to 212 labelled b(0)
212 to 213 labelled a(0)
213 to 214 labelled a(0)
214 to 215 labelled a(0)
215 to 203 labelled b(0)
202 to 214 labelled A(0)
202 to 207 labelled A(0)
202 to 216 labelled A(1)
216 to 217 labelled a(1)
217 to 203 labelled b(1)
202 to 218 labelled A(1)
218 to 219 labelled a(1)
219 to 220 labelled b(1)
220 to 221 labelled a(1)
221 to 222 labelled a(1)
222 to 223 labelled b(1)
223 to 224 labelled a(1)
224 to 225 labelled a(1)
225 to 226 labelled a(1)
226 to 203 labelled b(1)
202 to 227 labelled A(1)
227 to 228 labelled a(1)
228 to 229 labelled b(1)
229 to 230 labelled a(1)
230 to 231 labelled a(1)
231 to 232 labelled b(1)
232 to 233 labelled a(1)
233 to 234 labelled a(1)
234 to 235 labelled b(1)
235 to 236 labelled a(1)
236 to 237 labelled a(1)
237 to 238 labelled a(1)
238 to 203 labelled b(1)
213 to 219 labelled a(1)
206 to 239 labelled a(1)
239 to 240 labelled b(1)
240 to 241 labelled a(1)
241 to 242 labelled a(1)
242 to 243 labelled b(1)
243 to 244 labelled a(1)
244 to 245 labelled a(1)
245 to 246 labelled a(1)
246 to 213 labelled b(1)
202 to 245 labelled A(1)
217 to 210 labelled b(1)
236 to 219 labelled a(1)
224 to 219 labelled a(1)
202 to 221 labelled A(1)
229 to 247 labelled a(2)
247 to 248 labelled b(2)
248 to 249 labelled a(2)
249 to 250 labelled a(2)
250 to 251 labelled b(2)
251 to 252 labelled a(2)
252 to 253 labelled a(2)
253 to 254 labelled a(2)
254 to 236 labelled b(2)
209 to 255 labelled a(1)
255 to 256 labelled b(1)
256 to 257 labelled a(1)
257 to 258 labelled a(1)
258 to 259 labelled b(1)
259 to 260 labelled a(1)
260 to 261 labelled a(1)
261 to 262 labelled a(1)
262 to 221 labelled b(1)
244 to 219 labelled a(1)
202 to 263 labelled A(2)
263 to 264 labelled a(2)
264 to 233 labelled b(2)
264 to 224 labelled b(2)
212 to 265 labelled a(1)
265 to 266 labelled b(1)
266 to 267 labelled a(1)
267 to 268 labelled a(1)
268 to 269 labelled b(1)
269 to 270 labelled a(1)
270 to 271 labelled a(1)
271 to 272 labelled a(1)
272 to 224 labelled b(1)
217 to 255 labelled b(1)
232 to 273 labelled a(2)
273 to 274 labelled b(2)
274 to 275 labelled a(2)
275 to 276 labelled a(2)
276 to 277 labelled b(2)
277 to 278 labelled a(2)
278 to 279 labelled a(2)
279 to 280 labelled a(2)
280 to 221 labelled b(2)
220 to 273 labelled a(2)
202 to 279 labelled A(2)
240 to 273 labelled a(2)
270 to 219 labelled a(1)
252 to 219 labelled a(1)
235 to 281 labelled a(2)
281 to 282 labelled b(2)
282 to 283 labelled a(2)
283 to 284 labelled a(2)
284 to 285 labelled b(2)
285 to 286 labelled a(2)
286 to 287 labelled a(2)
287 to 288 labelled a(2)
288 to 224 labelled b(2)
223 to 281 labelled a(2)
243 to 281 labelled a(2)
217 to 265 labelled b(1)
246 to 265 labelled b(1)
288 to 281 labelled b(2)
269 to 281 labelled a(2)
251 to 281 labelled a(2)
202 to 287 labelled A(2)
272 to 281 labelled b(1)
266 to 273 labelled a(2)
248 to 273 labelled a(2)
229 to 281 labelled a(2)
264 to 273 labelled b(2)
286 to 219 labelled a(1)
280 to 273 labelled b(2)
262 to 273 labelled b(1)
285 to 281 labelled a(2)
282 to 273 labelled a(2)

Termination of R successfully shown.
Duration:
0:14 minutes

POL(b(x₁))	= x₁
POL(a(x₁))	= x₁
POL(A(x₁))	= 1 + x₁