Termination w.r.t. Q of the given QTRS could be proven:

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

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)))))))))

Q is empty.

(1) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.

(2) Obligation:

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

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)

The TRS R consists of the following rules:

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)))))))))

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

(3) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 6 less nodes.

(4) Obligation:

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

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)))))))
F(a, f(a, f(b, f(a, f(a, f(b, f(a, x))))))) → F(a, f(a, f(b, x)))

The TRS R consists of the following rules:

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)))))))))

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

(5) UsableRulesReductionPairsProof (EQUIVALENT transformation)

First, we A-transformed [FROCOS05] the QDP-Problem. Then we obtain the following A-transformed DP problem.
The pairs P are:

a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))

and the Q and R are:
Q restricted rewrite system:
The TRS R consists of the following rules:

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

Q is empty.

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(a(x₁)) = x₁   
POL(a1(x₁)) = 2·x₁   
POL(b(x₁)) = x₁   

(6) Obligation:

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

a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))

The TRS R consists of the following rules:

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

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

(7) RFCMatchBoundsDPProof (EQUIVALENT transformation)

Finiteness of the DP problem can be shown by a matchbound of 2.
As the DP problem is minimal we only have to initialize the certificate graph by the rules of P:

a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))

To find matches we regarded all rules of R and P:

a(a(b(a(a(b(a(x))))))) → a(b(a(a(b(a(a(a(b(x)))))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(a(b(x))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(a(a(a(b(x)))))))
a1(a(b(a(a(b(a(x))))))) → a1(a(b(x)))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1135554, 1135555, 1135558, 1135559, 1135557, 1135556, 1135561, 1135560, 1135564, 1135565, 1135567, 1135562, 1135566, 1135563, 1135568, 1135573, 1135574, 1135570, 1135571, 1135572, 1135569, 1135575, 1135582, 1135583, 1135580, 1135581, 1135577, 1135578, 1135579, 1135576, 1135588, 1135589, 1135590, 1135584, 1135585, 1135591, 1135586, 1135587, 1135594, 1135595, 1135596, 1135599, 1135592, 1135593, 1135598, 1135597

Node 1135554 is start node and node 1135555 is final node.

Those nodes are connect through the following edges:

• 1135554 to 1135556 labelled a1_1(0)
• 1135554 to 1135560 labelled a1_1(0)
• 1135554 to 1135559 labelled a1_1(0)
• 1135554 to 1135562 labelled a1_1(1)
• 1135554 to 1135566 labelled a1_1(1)
• 1135554 to 1135565 labelled a1_1(1)
• 1135554 to 1135578 labelled a1_1(1)
• 1135554 to 1135582 labelled a1_1(1)
• 1135554 to 1135581 labelled a1_1(1)
• 1135554 to 1135586 labelled a1_1(2)
• 1135554 to 1135590 labelled a1_1(2)
• 1135554 to 1135589 labelled a1_1(2)
• 1135554 to 1135594 labelled a1_1(2)
• 1135554 to 1135598 labelled a1_1(2)
• 1135554 to 1135597 labelled a1_1(2)
• 1135555 to 1135555 labelled #_1(0)
• 1135558 to 1135559 labelled a_1(0)
• 1135558 to 1135576 labelled a_1(1)
• 1135559 to 1135560 labelled a_1(0)
• 1135559 to 1135568 labelled a_1(1)
• 1135557 to 1135558 labelled b_1(0)
• 1135556 to 1135557 labelled a_1(0)
• 1135561 to 1135555 labelled b_1(0)
• 1135560 to 1135561 labelled a_1(0)
• 1135564 to 1135565 labelled a_1(1)
• 1135564 to 1135584 labelled a_1(2)
• 1135565 to 1135566 labelled a_1(1)
• 1135565 to 1135568 labelled a_1(1)
• 1135567 to 1135555 labelled b_1(1)
• 1135567 to 1135570 labelled b_1(1)
• 1135567 to 1135592 labelled b_1(1)
• 1135562 to 1135563 labelled a_1(1)
• 1135566 to 1135567 labelled a_1(1)
• 1135563 to 1135564 labelled b_1(1)
• 1135568 to 1135569 labelled b_1(1)
• 1135573 to 1135574 labelled a_1(1)
• 1135573 to 1135568 labelled a_1(1)
• 1135574 to 1135575 labelled a_1(1)
• 1135570 to 1135571 labelled a_1(1)
• 1135571 to 1135572 labelled b_1(1)
• 1135572 to 1135573 labelled a_1(1)
• 1135572 to 1135584 labelled a_1(2)
• 1135569 to 1135570 labelled a_1(1)
• 1135569 to 1135592 labelled a_1(2)
• 1135575 to 1135555 labelled b_1(1)
• 1135582 to 1135583 labelled a_1(1)
• 1135583 to 1135573 labelled b_1(1)
• 1135583 to 1135584 labelled b_1(1)
• 1135580 to 1135581 labelled a_1(1)
• 1135580 to 1135584 labelled a_1(2)
• 1135581 to 1135582 labelled a_1(1)
• 1135581 to 1135568 labelled a_1(1)
• 1135577 to 1135578 labelled a_1(1)
• 1135577 to 1135592 labelled a_1(2)
• 1135578 to 1135579 labelled a_1(1)
• 1135579 to 1135580 labelled b_1(1)
• 1135576 to 1135577 labelled b_1(1)
• 1135588 to 1135589 labelled a_1(2)
• 1135588 to 1135584 labelled a_1(2)
• 1135589 to 1135590 labelled a_1(2)
• 1135589 to 1135568 labelled a_1(1)
• 1135590 to 1135591 labelled a_1(2)
• 1135584 to 1135585 labelled b_1(2)
• 1135585 to 1135586 labelled a_1(2)
• 1135585 to 1135592 labelled a_1(2)
• 1135591 to 1135573 labelled b_1(2)
• 1135591 to 1135584 labelled b_1(2)
• 1135586 to 1135587 labelled a_1(2)
• 1135587 to 1135588 labelled b_1(2)
• 1135594 to 1135595 labelled a_1(2)
• 1135595 to 1135596 labelled b_1(2)
• 1135596 to 1135597 labelled a_1(2)
• 1135599 to 1135570 labelled b_1(2)
• 1135599 to 1135592 labelled b_1(2)
• 1135592 to 1135593 labelled b_1(2)
• 1135593 to 1135594 labelled a_1(2)
• 1135598 to 1135599 labelled a_1(2)
• 1135597 to 1135598 labelled a_1(2)

(8) TRUE