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

Q is empty.

(1) AAECC Innermost (EQUIVALENT transformation)

We have applied [NOC,AAECCNOC] to switch to innermost. The TRS R 1 is none

The TRS R 2 is

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

The signature Sigma is {f}

(2) Obligation:

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

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

The set Q consists of the following terms:

f(x0, a(a(b(b(x1)))))
f(a(x0), x1)
f(b(x0), x1)

(3) DependencyPairsProof (EQUIVALENT transformation)

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

(4) Obligation:

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

F(x, a(a(b(b(y))))) → F(a(a(a(b(b(b(x)))))), y)
F(a(x), y) → F(x, a(y))
F(b(x), y) → F(x, b(y))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

f(x0, a(a(b(b(x1)))))
f(a(x0), x1)
f(b(x0), x1)

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

(5) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(6) Obligation:

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

F(x, a(a(b(b(y))))) → F(a(a(a(b(b(b(x)))))), y)
F(a(x), y) → F(x, a(y))
F(b(x), y) → F(x, b(y))

R is empty.
The set Q consists of the following terms:

f(x0, a(a(b(b(x1)))))
f(a(x0), x1)
f(b(x0), x1)

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

(7) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

f(x0, a(a(b(b(x1)))))
f(a(x0), x1)
f(b(x0), x1)

(8) Obligation:

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

F(x, a(a(b(b(y))))) → F(a(a(a(b(b(b(x)))))), y)
F(a(x), y) → F(x, a(y))
F(b(x), y) → F(x, b(y))

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

(9) QDPToSRSProof (SOUND transformation)

The finiteness of this DP problem is implied by strong termination of a SRS due to [UNKNOWN].

(10) Obligation:

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

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

Q is empty.

(11) DependencyPairsProof (EQUIVALENT transformation)

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

(12) Obligation:

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

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

The TRS R consists of the following rules:

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

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

(13) MNOCProof (EQUIVALENT transformation)

We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.

(14) Obligation:

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

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

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

a(a(b(b(x0))))

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

(15) Narrowing (EQUIVALENT transformation)

By narrowing [LPAR04] the rule A(a(b(b(x)))) → A(a(a(x))) at position [0] we obtained the following new rules [LPAR04]:

A(a(b(b(b(b(x0)))))) → A(b(b(b(a(a(a(x0)))))))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))

(16) Obligation:

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

A(a(b(b(x)))) → A(a(x))
A(a(b(b(x)))) → A(x)
A(a(b(b(b(b(x0)))))) → A(b(b(b(a(a(a(x0)))))))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

a(a(b(b(x0))))

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

(17) DependencyGraphProof (EQUIVALENT transformation)

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

(18) Obligation:

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

A(a(b(b(x)))) → A(x)
A(a(b(b(x)))) → A(a(x))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

a(a(b(b(x0))))

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

(19) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule A(a(b(b(x)))) → A(x) we obtained the following new rules [LPAR04]:

A(a(b(b(a(b(b(y_0))))))) → A(a(b(b(y_0))))
A(a(b(b(a(b(b(a(b(b(y_0)))))))))) → A(a(b(b(a(b(b(y_0)))))))

(20) Obligation:

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

A(a(b(b(x)))) → A(a(x))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))
A(a(b(b(a(b(b(y_0))))))) → A(a(b(b(y_0))))
A(a(b(b(a(b(b(a(b(b(y_0)))))))))) → A(a(b(b(a(b(b(y_0)))))))

The TRS R consists of the following rules:

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

The set Q consists of the following terms:

a(a(b(b(x0))))

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

(21) RFCMatchBoundsDPProof (EQUIVALENT transformation)

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

A(a(b(b(x)))) → A(a(x))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))
A(a(b(b(a(b(b(y_0))))))) → A(a(b(b(y_0))))
A(a(b(b(a(b(b(a(b(b(y_0)))))))))) → A(a(b(b(a(b(b(y_0)))))))

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

a(a(b(b(x)))) → b(b(b(a(a(a(x))))))
A(a(b(b(x)))) → A(a(x))
A(a(b(b(a(b(b(x0))))))) → A(a(b(b(b(a(a(a(x0))))))))
A(a(b(b(a(b(b(y_0))))))) → A(a(b(b(y_0))))
A(a(b(b(a(b(b(a(b(b(y_0)))))))))) → A(a(b(b(a(b(b(y_0)))))))

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1145583, 1145584, 1145585, 1145591, 1145592, 1145587, 1145588, 1145586, 1145590, 1145589, 1145593, 1145595, 1145596, 1145598, 1145597, 1145594, 1145602, 1145603, 1145600, 1145601, 1145599, 1145609, 1145610, 1145607, 1145608, 1145606, 1145604, 1145605, 1145616, 1145611, 1145613, 1145614, 1145615, 1145612, 1145617, 1145622, 1145618, 1145619, 1145620, 1145621, 1145629, 1145623, 1145624, 1145627, 1145628, 1145626, 1145625, 1145630, 1145635, 1145631, 1145632, 1145633, 1145634, 1145639, 1145640, 1145636, 1145638, 1145637, 1145645, 1145641, 1145642, 1145643, 1145644, 1145648, 1145649, 1145650, 1145646, 1145647, 1145655, 1145651, 1145652, 1145653, 1145654, 1145659, 1145660, 1145662, 1145661, 1145657, 1145658, 1145656, 1145663, 1145668, 1145665, 1145666, 1145664, 1145667, 1145673, 1145672, 1145669, 1145671, 1145670

Node 1145583 is start node and node 1145584 is final node.

Those nodes are connect through the following edges:

• 1145583 to 1145585 labelled A_1(0)
• 1145583 to 1145586 labelled A_1(0)
• 1145583 to 1145593 labelled A_1(0)
• 1145583 to 1145603 labelled A_1(1)
• 1145583 to 1145604 labelled A_1(1)
• 1145583 to 1145611 labelled A_1(1)
• 1145583 to 1145602 labelled A_1(1)
• 1145583 to 1145617 labelled A_1(2)
• 1145583 to 1145623 labelled A_1(2)
• 1145583 to 1145630 labelled A_1(3)
• 1145583 to 1145635 labelled A_1(2)
• 1145583 to 1145650 labelled A_1(3)
• 1145583 to 1145656 labelled A_1(3)
• 1145583 to 1145644 labelled A_1(2)
• 1145583 to 1145633 labelled A_1(2)
• 1145583 to 1145663 labelled A_1(4)
• 1145583 to 1145662 labelled A_1(3)
• 1145583 to 1145649 labelled A_1(3)
• 1145584 to 1145584 labelled #_1(0)
• 1145585 to 1145584 labelled a_1(0)
• 1145585 to 1145599 labelled b_1(1)
• 1145591 to 1145592 labelled a_1(0)
• 1145591 to 1145599 labelled b_1(1)
• 1145592 to 1145584 labelled a_1(0)
• 1145592 to 1145599 labelled b_1(1)
• 1145587 to 1145588 labelled b_1(0)
• 1145588 to 1145589 labelled b_1(0)
• 1145588 to 1145584 labelled b_1(0)
• 1145586 to 1145587 labelled a_1(0)
• 1145590 to 1145591 labelled a_1(0)
• 1145590 to 1145618 labelled b_1(1)
• 1145589 to 1145590 labelled b_1(0)
• 1145593 to 1145594 labelled a_1(0)
• 1145595 to 1145596 labelled b_1(0)
• 1145596 to 1145597 labelled a_1(0)
• 1145598 to 1145584 labelled b_1(0)
• 1145597 to 1145598 labelled b_1(0)
• 1145594 to 1145595 labelled b_1(0)
• 1145602 to 1145603 labelled a_1(1)
• 1145602 to 1145599 labelled b_1(1)
• 1145602 to 1145641 labelled b_1(2)
• 1145603 to 1145584 labelled a_1(1)
• 1145603 to 1145596 labelled a_1(1)
• 1145603 to 1145589 labelled a_1(1)
• 1145603 to 1145599 labelled b_1(1)
• 1145603 to 1145618 labelled a_1(1)
• 1145600 to 1145601 labelled b_1(1)
• 1145601 to 1145602 labelled a_1(1)
• 1145601 to 1145631 labelled b_1(2)
• 1145599 to 1145600 labelled b_1(1)
• 1145609 to 1145610 labelled a_1(1)
• 1145609 to 1145599 labelled b_1(1)
• 1145610 to 1145584 labelled a_1(1)
• 1145610 to 1145599 labelled b_1(1)
• 1145607 to 1145608 labelled b_1(1)
• 1145608 to 1145609 labelled a_1(1)
• 1145608 to 1145631 labelled b_1(2)
• 1145606 to 1145607 labelled b_1(1)
• 1145606 to 1145584 labelled b_1(1)
• 1145604 to 1145605 labelled a_1(1)
• 1145605 to 1145606 labelled b_1(1)
• 1145616 to 1145584 labelled b_1(1)
• 1145611 to 1145612 labelled a_1(1)
• 1145613 to 1145614 labelled b_1(1)
• 1145614 to 1145615 labelled a_1(1)
• 1145615 to 1145616 labelled b_1(1)
• 1145612 to 1145613 labelled b_1(1)
• 1145617 to 1145607 labelled a_1(2)
• 1145617 to 1145614 labelled a_1(2)
• 1145617 to 1145584 labelled a_1(2)
• 1145617 to 1145599 labelled b_1(1)
• 1145617 to 1145625 labelled b_1(2)
• 1145617 to 1145631 labelled a_1(2)
• 1145617 to 1145620 labelled a_1(2)
• 1145617 to 1145651 labelled b_1(2)
• 1145622 to 1145600 labelled a_1(1)
• 1145618 to 1145619 labelled b_1(1)
• 1145619 to 1145620 labelled b_1(1)
• 1145620 to 1145621 labelled a_1(1)
• 1145621 to 1145622 labelled a_1(1)
• 1145621 to 1145636 labelled b_1(2)
• 1145629 to 1145584 labelled a_1(2)
• 1145629 to 1145599 labelled b_1(1)
• 1145623 to 1145624 labelled a_1(2)
• 1145624 to 1145625 labelled b_1(2)
• 1145627 to 1145628 labelled a_1(2)
• 1145627 to 1145631 labelled b_1(2)
• 1145628 to 1145629 labelled a_1(2)
• 1145628 to 1145599 labelled b_1(1)
• 1145626 to 1145627 labelled b_1(2)
• 1145625 to 1145626 labelled b_1(2)
• 1145625 to 1145584 labelled b_1(2)
• 1145630 to 1145584 labelled a_1(3)
• 1145630 to 1145626 labelled a_1(3)
• 1145630 to 1145599 labelled b_1(1)
• 1145630 to 1145631 labelled a_1(3)
• 1145630 to 1145652 labelled a_1(3)
• 1145635 to 1145600 labelled a_1(2)
• 1145631 to 1145632 labelled b_1(2)
• 1145632 to 1145633 labelled b_1(2)
• 1145633 to 1145634 labelled a_1(2)
• 1145634 to 1145635 labelled a_1(2)
• 1145634 to 1145636 labelled b_1(2)
• 1145639 to 1145640 labelled a_1(2)
• 1145639 to 1145646 labelled b_1(3)
• 1145640 to 1145631 labelled a_1(2)
• 1145636 to 1145637 labelled b_1(2)
• 1145638 to 1145639 labelled a_1(2)
• 1145637 to 1145638 labelled b_1(2)
• 1145645 to 1145620 labelled a_1(2)
• 1145645 to 1145651 labelled b_1(2)
• 1145641 to 1145642 labelled b_1(2)
• 1145642 to 1145643 labelled b_1(2)
• 1145643 to 1145644 labelled a_1(2)
• 1145643 to 1145664 labelled b_1(3)
• 1145644 to 1145645 labelled a_1(2)
• 1145648 to 1145649 labelled a_1(3)
• 1145648 to 1145669 labelled b_1(4)
• 1145649 to 1145650 labelled a_1(3)
• 1145650 to 1145633 labelled a_1(3)
• 1145650 to 1145658 labelled b_1(3)
• 1145646 to 1145647 labelled b_1(3)
• 1145647 to 1145648 labelled b_1(3)
• 1145655 to 1145637 labelled a_1(2)
• 1145651 to 1145652 labelled b_1(2)
• 1145652 to 1145653 labelled b_1(2)
• 1145653 to 1145654 labelled a_1(2)
• 1145654 to 1145655 labelled a_1(2)
• 1145659 to 1145660 labelled b_1(3)
• 1145660 to 1145661 labelled a_1(3)
• 1145662 to 1145637 labelled a_1(3)
• 1145661 to 1145662 labelled a_1(3)
• 1145657 to 1145658 labelled b_1(3)
• 1145658 to 1145659 labelled b_1(3)
• 1145658 to 1145637 labelled b_1(3)
• 1145656 to 1145657 labelled a_1(3)
• 1145663 to 1145637 labelled a_1(4)
• 1145663 to 1145659 labelled a_1(4)
• 1145668 to 1145652 labelled a_1(3)
• 1145665 to 1145666 labelled b_1(3)
• 1145666 to 1145667 labelled a_1(3)
• 1145664 to 1145665 labelled b_1(3)
• 1145667 to 1145668 labelled a_1(3)
• 1145673 to 1145637 labelled a_1(4)
• 1145673 to 1145659 labelled a_1(4)
• 1145672 to 1145673 labelled a_1(4)
• 1145669 to 1145670 labelled b_1(4)
• 1145671 to 1145672 labelled a_1(4)
• 1145670 to 1145671 labelled b_1(4)

(22) TRUE