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

0 QTRS
↳1 DependencyPairsProof (⇔)
↳2 QDP
↳3 DependencyGraphProof (⇔)
↳4 QDP
↳5 UsableRulesReductionPairsProof (⇔)
↳6 QDP
↳7 RFCMatchBoundsDPProof (⇔)
↳8 TRUE

(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(x1)) = x1   
POL(a1(x1)) = 2·x1   
POL(b(x1)) = x1   

(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:

7405894, 7405895, 7405900, 7405901, 7405898, 7405899, 7405896, 7405897, 7405906, 7405907, 7405903, 7405904, 7405902, 7405905, 7405908, 7405909, 7405911, 7405912, 7405913, 7405914, 7405915, 7405910, 7405921, 7405922, 7405923, 7405919, 7405920, 7405918, 7405917, 7405916, 7405929, 7405930, 7405928, 7405924, 7405925, 7405931, 7405926, 7405927

Node 7405894 is start node and node 7405895 is final node.

Those nodes are connect through the following edges:

  • 7405894 to 7405896 labelled a1_1(0)
  • 7405894 to 7405900 labelled a1_1(0)
  • 7405894 to 7405899 labelled a1_1(0)
  • 7405894 to 7405902 labelled a1_1(1)
  • 7405894 to 7405906 labelled a1_1(1)
  • 7405894 to 7405905 labelled a1_1(1)
  • 7405894 to 7405914 labelled a1_1(1)
  • 7405894 to 7405913 labelled a1_1(1)
  • 7405894 to 7405926 labelled a1_1(2)
  • 7405894 to 7405930 labelled a1_1(2)
  • 7405894 to 7405929 labelled a1_1(2)
  • 7405895 to 7405895 labelled #_1(0)
  • 7405900 to 7405901 labelled a_1(0)
  • 7405901 to 7405895 labelled b_1(0)
  • 7405898 to 7405899 labelled a_1(0)
  • 7405898 to 7405916 labelled a_1(1)
  • 7405899 to 7405900 labelled a_1(0)
  • 7405899 to 7405908 labelled a_1(1)
  • 7405896 to 7405897 labelled a_1(0)
  • 7405897 to 7405898 labelled b_1(0)
  • 7405906 to 7405907 labelled a_1(1)
  • 7405907 to 7405895 labelled b_1(1)
  • 7405907 to 7405913 labelled b_1(1)
  • 7405907 to 7405910 labelled b_1(1)
  • 7405907 to 7405924 labelled b_1(1)
  • 7405903 to 7405904 labelled b_1(1)
  • 7405904 to 7405905 labelled a_1(1)
  • 7405904 to 7405924 labelled a_1(2)
  • 7405902 to 7405903 labelled a_1(1)
  • 7405905 to 7405906 labelled a_1(1)
  • 7405905 to 7405908 labelled a_1(1)
  • 7405908 to 7405909 labelled b_1(1)
  • 7405909 to 7405910 labelled a_1(1)
  • 7405909 to 7405924 labelled a_1(2)
  • 7405911 to 7405912 labelled b_1(1)
  • 7405912 to 7405913 labelled a_1(1)
  • 7405912 to 7405924 labelled a_1(2)
  • 7405913 to 7405914 labelled a_1(1)
  • 7405913 to 7405908 labelled a_1(1)
  • 7405914 to 7405915 labelled a_1(1)
  • 7405915 to 7405895 labelled b_1(1)
  • 7405910 to 7405911 labelled a_1(1)
  • 7405921 to 7405922 labelled a_1(1)
  • 7405921 to 7405908 labelled a_1(1)
  • 7405922 to 7405923 labelled a_1(1)
  • 7405923 to 7405913 labelled b_1(1)
  • 7405923 to 7405924 labelled b_1(1)
  • 7405919 to 7405920 labelled b_1(1)
  • 7405920 to 7405921 labelled a_1(1)
  • 7405920 to 7405924 labelled a_1(2)
  • 7405918 to 7405919 labelled a_1(1)
  • 7405917 to 7405918 labelled a_1(1)
  • 7405917 to 7405924 labelled a_1(2)
  • 7405916 to 7405917 labelled b_1(1)
  • 7405929 to 7405930 labelled a_1(2)
  • 7405929 to 7405908 labelled a_1(1)
  • 7405930 to 7405931 labelled a_1(2)
  • 7405928 to 7405929 labelled a_1(2)
  • 7405928 to 7405924 labelled a_1(2)
  • 7405924 to 7405925 labelled b_1(2)
  • 7405925 to 7405926 labelled a_1(2)
  • 7405925 to 7405924 labelled a_1(2)
  • 7405931 to 7405913 labelled b_1(2)
  • 7405931 to 7405910 labelled b_1(2)
  • 7405931 to 7405924 labelled b_1(2)
  • 7405926 to 7405927 labelled a_1(2)
  • 7405927 to 7405928 labelled b_1(2)

(8) TRUE