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:

7415823, 7415824, 7415825, 7415826, 7415827, 7415831, 7415832, 7415828, 7415830, 7415829, 7415836, 7415837, 7415833, 7415834, 7415835, 7415838, 7415839, 7415842, 7415843, 7415840, 7415841, 7415846, 7415847, 7415850, 7415848, 7415849, 7415844, 7415845, 7415851, 7415855, 7415856, 7415852, 7415853, 7415854, 7415857, 7415858, 7415860, 7415861, 7415859, 7415862, 7415868, 7415869, 7415863, 7415864, 7415865, 7415866, 7415867, 7415874, 7415872, 7415873, 7415870, 7415871, 7415875, 7415876, 7415878, 7415879, 7415877, 7415880, 7415885, 7415884, 7415883, 7415882, 7415881, 7415887, 7415888, 7415889, 7415890, 7415886, 7415895, 7415893, 7415894, 7415891, 7415892, 7415896, 7415902, 7415901, 7415897, 7415898, 7415899, 7415900, 7415903, 7415904, 7415905, 7415907, 7415908, 7415906, 7415912, 7415913, 7415909, 7415910, 7415911

Node 7415823 is start node and node 7415824 is final node.

Those nodes are connect through the following edges:

• 7415823 to 7415825 labelled A_1(0)
• 7415823 to 7415826 labelled A_1(0)
• 7415823 to 7415833 labelled A_1(0)
• 7415823 to 7415843 labelled A_1(1)
• 7415823 to 7415844 labelled A_1(1)
• 7415823 to 7415851 labelled A_1(1)
• 7415823 to 7415854 labelled A_1(1)
• 7415823 to 7415848 labelled A_1(1)
• 7415823 to 7415857 labelled A_1(2)
• 7415823 to 7415863 labelled A_1(2)
• 7415823 to 7415875 labelled A_1(3)
• 7415823 to 7415885 labelled A_1(2)
• 7415823 to 7415884 labelled A_1(2)
• 7415823 to 7415872 labelled A_1(2)
• 7415823 to 7415896 labelled A_1(3)
• 7415823 to 7415903 labelled A_1(4)
• 7415823 to 7415902 labelled A_1(3)
• 7415824 to 7415824 labelled #_1(0)
• 7415825 to 7415824 labelled a_1(0)
• 7415825 to 7415839 labelled b_1(1)
• 7415826 to 7415827 labelled a_1(0)
• 7415827 to 7415828 labelled b_1(0)
• 7415831 to 7415832 labelled a_1(0)
• 7415831 to 7415839 labelled b_1(1)
• 7415832 to 7415824 labelled a_1(0)
• 7415832 to 7415839 labelled b_1(1)
• 7415828 to 7415829 labelled b_1(0)
• 7415828 to 7415824 labelled b_1(0)
• 7415830 to 7415831 labelled a_1(0)
• 7415830 to 7415858 labelled b_1(1)
• 7415829 to 7415830 labelled b_1(0)
• 7415836 to 7415837 labelled a_1(0)
• 7415837 to 7415838 labelled b_1(0)
• 7415833 to 7415834 labelled a_1(0)
• 7415834 to 7415835 labelled b_1(0)
• 7415835 to 7415836 labelled b_1(0)
• 7415838 to 7415824 labelled b_1(0)
• 7415839 to 7415840 labelled b_1(1)
• 7415842 to 7415843 labelled a_1(1)
• 7415842 to 7415839 labelled b_1(1)
• 7415842 to 7415881 labelled b_1(2)
• 7415843 to 7415824 labelled a_1(1)
• 7415843 to 7415836 labelled a_1(1)
• 7415843 to 7415829 labelled a_1(1)
• 7415843 to 7415839 labelled b_1(1)
• 7415843 to 7415858 labelled a_1(1)
• 7415840 to 7415841 labelled b_1(1)
• 7415841 to 7415842 labelled a_1(1)
• 7415841 to 7415870 labelled b_1(2)
• 7415846 to 7415847 labelled b_1(1)
• 7415846 to 7415824 labelled b_1(1)
• 7415847 to 7415848 labelled b_1(1)
• 7415850 to 7415824 labelled a_1(1)
• 7415850 to 7415839 labelled b_1(1)
• 7415848 to 7415849 labelled a_1(1)
• 7415848 to 7415870 labelled b_1(2)
• 7415849 to 7415850 labelled a_1(1)
• 7415849 to 7415839 labelled b_1(1)
• 7415844 to 7415845 labelled a_1(1)
• 7415845 to 7415846 labelled b_1(1)
• 7415851 to 7415852 labelled a_1(1)
• 7415855 to 7415856 labelled b_1(1)
• 7415856 to 7415824 labelled b_1(1)
• 7415852 to 7415853 labelled b_1(1)
• 7415853 to 7415854 labelled b_1(1)
• 7415854 to 7415855 labelled a_1(1)
• 7415857 to 7415847 labelled a_1(2)
• 7415857 to 7415824 labelled a_1(2)
• 7415857 to 7415854 labelled a_1(2)
• 7415857 to 7415839 labelled b_1(1)
• 7415857 to 7415840 labelled a_1(2)
• 7415857 to 7415865 labelled b_1(2)
• 7415857 to 7415870 labelled a_1(2)
• 7415858 to 7415859 labelled b_1(1)
• 7415860 to 7415861 labelled a_1(1)
• 7415861 to 7415862 labelled a_1(1)
• 7415861 to 7415876 labelled b_1(2)
• 7415859 to 7415860 labelled b_1(1)
• 7415862 to 7415840 labelled a_1(1)
• 7415868 to 7415869 labelled a_1(2)
• 7415868 to 7415839 labelled b_1(1)
• 7415869 to 7415824 labelled a_1(2)
• 7415869 to 7415839 labelled b_1(1)
• 7415863 to 7415864 labelled a_1(2)
• 7415864 to 7415865 labelled b_1(2)
• 7415865 to 7415866 labelled b_1(2)
• 7415865 to 7415824 labelled b_1(2)
• 7415866 to 7415867 labelled b_1(2)
• 7415867 to 7415868 labelled a_1(2)
• 7415867 to 7415870 labelled b_1(2)
• 7415874 to 7415840 labelled a_1(2)
• 7415872 to 7415873 labelled a_1(2)
• 7415873 to 7415874 labelled a_1(2)
• 7415873 to 7415876 labelled b_1(2)
• 7415870 to 7415871 labelled b_1(2)
• 7415871 to 7415872 labelled b_1(2)
• 7415875 to 7415866 labelled a_1(3)
• 7415875 to 7415824 labelled a_1(3)
• 7415875 to 7415839 labelled b_1(1)
• 7415875 to 7415872 labelled a_1(3)
• 7415875 to 7415870 labelled a_1(3)
• 7415875 to 7415892 labelled a_1(3)
• 7415875 to 7415898 labelled b_1(3)
• 7415876 to 7415877 labelled b_1(2)
• 7415878 to 7415879 labelled a_1(2)
• 7415879 to 7415880 labelled a_1(2)
• 7415879 to 7415886 labelled b_1(3)
• 7415877 to 7415878 labelled b_1(2)
• 7415880 to 7415870 labelled a_1(2)
• 7415885 to 7415860 labelled a_1(2)
• 7415885 to 7415891 labelled b_1(2)
• 7415884 to 7415885 labelled a_1(2)
• 7415883 to 7415884 labelled a_1(2)
• 7415883 to 7415904 labelled b_1(3)
• 7415882 to 7415883 labelled b_1(2)
• 7415881 to 7415882 labelled b_1(2)
• 7415887 to 7415888 labelled b_1(3)
• 7415888 to 7415889 labelled a_1(3)
• 7415888 to 7415909 labelled b_1(4)
• 7415889 to 7415890 labelled a_1(3)
• 7415890 to 7415872 labelled a_1(3)
• 7415890 to 7415898 labelled b_1(3)
• 7415886 to 7415887 labelled b_1(3)
• 7415895 to 7415877 labelled a_1(2)
• 7415893 to 7415894 labelled a_1(2)
• 7415894 to 7415895 labelled a_1(2)
• 7415891 to 7415892 labelled b_1(2)
• 7415892 to 7415893 labelled b_1(2)
• 7415896 to 7415897 labelled a_1(3)
• 7415902 to 7415877 labelled a_1(3)
• 7415901 to 7415902 labelled a_1(3)
• 7415897 to 7415898 labelled b_1(3)
• 7415898 to 7415899 labelled b_1(3)
• 7415898 to 7415877 labelled b_1(3)
• 7415899 to 7415900 labelled b_1(3)
• 7415900 to 7415901 labelled a_1(3)
• 7415903 to 7415877 labelled a_1(4)
• 7415903 to 7415899 labelled a_1(4)
• 7415904 to 7415905 labelled b_1(3)
• 7415905 to 7415906 labelled b_1(3)
• 7415907 to 7415908 labelled a_1(3)
• 7415908 to 7415892 labelled a_1(3)
• 7415906 to 7415907 labelled a_1(3)
• 7415912 to 7415913 labelled a_1(4)
• 7415913 to 7415877 labelled a_1(4)
• 7415913 to 7415899 labelled a_1(4)
• 7415909 to 7415910 labelled b_1(4)
• 7415910 to 7415911 labelled b_1(4)
• 7415911 to 7415912 labelled a_1(4)

(22) TRUE