YES Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema_04/z080.srs

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

0 QTRS
↳1 FlatCCProof (⇔, 0 ms)
↳2 QTRS
↳3 RootLabelingProof (⇔, 0 ms)
↳4 QTRS
↳5 QTRSRRRProof (⇔, 67 ms)
↳6 QTRS
↳7 QTRSRRRProof (⇔, 19 ms)
↳8 QTRS
↳9 DependencyPairsProof (⇔, 37 ms)
↳10 QDP
↳11 QDPOrderProof (⇔, 165 ms)
↳12 QDP
↳13 DependencyGraphProof (⇔, 0 ms)
↳14 TRUE

(0) Obligation:

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

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

Q is empty.

(1) FlatCCProof (EQUIVALENT transformation)

We used flat context closure [ROOTLAB] As Q is empty the flat context closure was sound AND complete.

(2) Obligation:

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

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

Q is empty.

(3) RootLabelingProof (EQUIVALENT transformation)

We used plain root labeling [ROOTLAB] with the following heuristic: LabelAll: All function symbols get labeled
As Q is empty the root labeling was sound AND complete.

(4) Obligation:

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

A_{A_1}(A_{b_1}(b_{A_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
A_{A_1}(A_{b_1}(b_{b_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
A_{A_1}(A_{b_1}(b_{a_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
A_{A_1}(A_{b_1}(b_{B_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
b_{A_1}(A_{b_1}(b_{A_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
b_{A_1}(A_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
b_{A_1}(A_{b_1}(b_{a_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
b_{A_1}(A_{b_1}(b_{B_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
a_{A_1}(A_{b_1}(b_{A_1}(x))) → a_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
a_{A_1}(A_{b_1}(b_{b_1}(x))) → a_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
a_{A_1}(A_{b_1}(b_{a_1}(x))) → a_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
a_{A_1}(A_{b_1}(b_{B_1}(x))) → a_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
B_{A_1}(A_{b_1}(b_{A_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
B_{A_1}(A_{b_1}(b_{b_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
B_{A_1}(A_{b_1}(b_{a_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
B_{A_1}(A_{b_1}(b_{B_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
A_{B_1}(B_{a_1}(a_{A_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{A_1}(x)))))
A_{B_1}(B_{a_1}(a_{b_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
A_{B_1}(B_{a_1}(a_{a_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
A_{B_1}(B_{a_1}(a_{B_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
b_{B_1}(B_{a_1}(a_{A_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{A_1}(x)))))
b_{B_1}(B_{a_1}(a_{b_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
b_{B_1}(B_{a_1}(a_{a_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
b_{B_1}(B_{a_1}(a_{B_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
a_{B_1}(B_{a_1}(a_{A_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{A_1}(x)))))
a_{B_1}(B_{a_1}(a_{b_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
a_{B_1}(B_{a_1}(a_{a_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
a_{B_1}(B_{a_1}(a_{B_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
B_{B_1}(B_{a_1}(a_{A_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{A_1}(x)))))
B_{B_1}(B_{a_1}(a_{b_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
B_{B_1}(B_{a_1}(a_{a_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
B_{B_1}(B_{a_1}(a_{B_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
A_{A_1}(A_{a_1}(a_{A_1}(x))) → A_{A_1}(x)
A_{A_1}(A_{a_1}(a_{b_1}(x))) → A_{b_1}(x)
A_{A_1}(A_{a_1}(a_{a_1}(x))) → A_{a_1}(x)
A_{A_1}(A_{a_1}(a_{B_1}(x))) → A_{B_1}(x)
b_{A_1}(A_{a_1}(a_{A_1}(x))) → b_{A_1}(x)
b_{A_1}(A_{a_1}(a_{b_1}(x))) → b_{b_1}(x)
b_{A_1}(A_{a_1}(a_{a_1}(x))) → b_{a_1}(x)
b_{A_1}(A_{a_1}(a_{B_1}(x))) → b_{B_1}(x)
a_{A_1}(A_{a_1}(a_{A_1}(x))) → a_{A_1}(x)
a_{A_1}(A_{a_1}(a_{b_1}(x))) → a_{b_1}(x)
a_{A_1}(A_{a_1}(a_{a_1}(x))) → a_{a_1}(x)
a_{A_1}(A_{a_1}(a_{B_1}(x))) → a_{B_1}(x)
B_{A_1}(A_{a_1}(a_{A_1}(x))) → B_{A_1}(x)
B_{A_1}(A_{a_1}(a_{b_1}(x))) → B_{b_1}(x)
B_{A_1}(A_{a_1}(a_{a_1}(x))) → B_{a_1}(x)
B_{A_1}(A_{a_1}(a_{B_1}(x))) → B_{B_1}(x)
A_{B_1}(B_{b_1}(b_{A_1}(x))) → A_{A_1}(x)
A_{B_1}(B_{b_1}(b_{b_1}(x))) → A_{b_1}(x)
A_{B_1}(B_{b_1}(b_{a_1}(x))) → A_{a_1}(x)
A_{B_1}(B_{b_1}(b_{B_1}(x))) → A_{B_1}(x)
b_{B_1}(B_{b_1}(b_{A_1}(x))) → b_{A_1}(x)
b_{B_1}(B_{b_1}(b_{b_1}(x))) → b_{b_1}(x)
b_{B_1}(B_{b_1}(b_{a_1}(x))) → b_{a_1}(x)
b_{B_1}(B_{b_1}(b_{B_1}(x))) → b_{B_1}(x)
a_{B_1}(B_{b_1}(b_{A_1}(x))) → a_{A_1}(x)
a_{B_1}(B_{b_1}(b_{b_1}(x))) → a_{b_1}(x)
a_{B_1}(B_{b_1}(b_{a_1}(x))) → a_{a_1}(x)
a_{B_1}(B_{b_1}(b_{B_1}(x))) → a_{B_1}(x)
B_{B_1}(B_{b_1}(b_{A_1}(x))) → B_{A_1}(x)
B_{B_1}(B_{b_1}(b_{b_1}(x))) → B_{b_1}(x)
B_{B_1}(B_{b_1}(b_{a_1}(x))) → B_{a_1}(x)
B_{B_1}(B_{b_1}(b_{B_1}(x))) → B_{B_1}(x)

Q is empty.

(5) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(A_{A_1}(x1)) = 1 + x1   
POL(A_{B_1}(x1)) = x1   
POL(A_{a_1}(x1)) = x1   
POL(A_{b_1}(x1)) = 1 + x1   
POL(B_{A_1}(x1)) = x1   
POL(B_{B_1}(x1)) = 1 + x1   
POL(B_{a_1}(x1)) = 1 + x1   
POL(B_{b_1}(x1)) = x1   
POL(a_{A_1}(x1)) = 1 + x1   
POL(a_{B_1}(x1)) = 1 + x1   
POL(a_{a_1}(x1)) = 1 + x1   
POL(a_{b_1}(x1)) = x1   
POL(b_{A_1}(x1)) = 1 + x1   
POL(b_{B_1}(x1)) = x1   
POL(b_{a_1}(x1)) = x1   
POL(b_{b_1}(x1)) = 1 + x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

a_{A_1}(A_{b_1}(b_{A_1}(x))) → a_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
a_{A_1}(A_{b_1}(b_{b_1}(x))) → a_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
a_{A_1}(A_{b_1}(b_{a_1}(x))) → a_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
a_{A_1}(A_{b_1}(b_{B_1}(x))) → a_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
A_{B_1}(B_{a_1}(a_{A_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{A_1}(x)))))
b_{B_1}(B_{a_1}(a_{A_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{A_1}(x)))))
a_{B_1}(B_{a_1}(a_{A_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{A_1}(x)))))
B_{B_1}(B_{a_1}(a_{A_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{A_1}(x)))))
A_{A_1}(A_{a_1}(a_{A_1}(x))) → A_{A_1}(x)
A_{A_1}(A_{a_1}(a_{a_1}(x))) → A_{a_1}(x)
A_{A_1}(A_{a_1}(a_{B_1}(x))) → A_{B_1}(x)
b_{A_1}(A_{a_1}(a_{A_1}(x))) → b_{A_1}(x)
b_{A_1}(A_{a_1}(a_{a_1}(x))) → b_{a_1}(x)
b_{A_1}(A_{a_1}(a_{B_1}(x))) → b_{B_1}(x)
a_{A_1}(A_{a_1}(a_{A_1}(x))) → a_{A_1}(x)
a_{A_1}(A_{a_1}(a_{b_1}(x))) → a_{b_1}(x)
a_{A_1}(A_{a_1}(a_{a_1}(x))) → a_{a_1}(x)
a_{A_1}(A_{a_1}(a_{B_1}(x))) → a_{B_1}(x)
B_{A_1}(A_{a_1}(a_{A_1}(x))) → B_{A_1}(x)
a_{B_1}(B_{b_1}(b_{A_1}(x))) → a_{A_1}(x)
a_{B_1}(B_{b_1}(b_{b_1}(x))) → a_{b_1}(x)
B_{B_1}(B_{b_1}(b_{A_1}(x))) → B_{A_1}(x)
B_{B_1}(B_{b_1}(b_{b_1}(x))) → B_{b_1}(x)


(6) Obligation:

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

A_{A_1}(A_{b_1}(b_{A_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
A_{A_1}(A_{b_1}(b_{b_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
A_{A_1}(A_{b_1}(b_{a_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
A_{A_1}(A_{b_1}(b_{B_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
b_{A_1}(A_{b_1}(b_{A_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
b_{A_1}(A_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
b_{A_1}(A_{b_1}(b_{a_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
b_{A_1}(A_{b_1}(b_{B_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
B_{A_1}(A_{b_1}(b_{A_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
B_{A_1}(A_{b_1}(b_{b_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
B_{A_1}(A_{b_1}(b_{a_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
B_{A_1}(A_{b_1}(b_{B_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
A_{B_1}(B_{a_1}(a_{b_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
A_{B_1}(B_{a_1}(a_{a_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
A_{B_1}(B_{a_1}(a_{B_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
b_{B_1}(B_{a_1}(a_{b_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
b_{B_1}(B_{a_1}(a_{a_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
b_{B_1}(B_{a_1}(a_{B_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
a_{B_1}(B_{a_1}(a_{b_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
a_{B_1}(B_{a_1}(a_{a_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
a_{B_1}(B_{a_1}(a_{B_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
B_{B_1}(B_{a_1}(a_{b_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
B_{B_1}(B_{a_1}(a_{a_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
B_{B_1}(B_{a_1}(a_{B_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
A_{A_1}(A_{a_1}(a_{b_1}(x))) → A_{b_1}(x)
b_{A_1}(A_{a_1}(a_{b_1}(x))) → b_{b_1}(x)
B_{A_1}(A_{a_1}(a_{b_1}(x))) → B_{b_1}(x)
B_{A_1}(A_{a_1}(a_{a_1}(x))) → B_{a_1}(x)
B_{A_1}(A_{a_1}(a_{B_1}(x))) → B_{B_1}(x)
A_{B_1}(B_{b_1}(b_{A_1}(x))) → A_{A_1}(x)
A_{B_1}(B_{b_1}(b_{b_1}(x))) → A_{b_1}(x)
A_{B_1}(B_{b_1}(b_{a_1}(x))) → A_{a_1}(x)
A_{B_1}(B_{b_1}(b_{B_1}(x))) → A_{B_1}(x)
b_{B_1}(B_{b_1}(b_{A_1}(x))) → b_{A_1}(x)
b_{B_1}(B_{b_1}(b_{b_1}(x))) → b_{b_1}(x)
b_{B_1}(B_{b_1}(b_{a_1}(x))) → b_{a_1}(x)
b_{B_1}(B_{b_1}(b_{B_1}(x))) → b_{B_1}(x)
a_{B_1}(B_{b_1}(b_{a_1}(x))) → a_{a_1}(x)
a_{B_1}(B_{b_1}(b_{B_1}(x))) → a_{B_1}(x)
B_{B_1}(B_{b_1}(b_{a_1}(x))) → B_{a_1}(x)
B_{B_1}(B_{b_1}(b_{B_1}(x))) → B_{B_1}(x)

Q is empty.

(7) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Polynomial interpretation [POLO]:

POL(A_{A_1}(x1)) = x1   
POL(A_{B_1}(x1)) = x1   
POL(A_{a_1}(x1)) = x1   
POL(A_{b_1}(x1)) = x1   
POL(B_{A_1}(x1)) = x1   
POL(B_{B_1}(x1)) = x1   
POL(B_{a_1}(x1)) = x1   
POL(B_{b_1}(x1)) = x1   
POL(a_{B_1}(x1)) = x1   
POL(a_{a_1}(x1)) = x1   
POL(a_{b_1}(x1)) = x1   
POL(b_{A_1}(x1)) = x1   
POL(b_{B_1}(x1)) = 1 + x1   
POL(b_{a_1}(x1)) = x1   
POL(b_{b_1}(x1)) = x1   
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

A_{A_1}(A_{b_1}(b_{B_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
b_{A_1}(A_{b_1}(b_{B_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
B_{A_1}(A_{b_1}(b_{B_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{B_1}(x)))))
b_{B_1}(B_{a_1}(a_{b_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
b_{B_1}(B_{a_1}(a_{a_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
b_{B_1}(B_{a_1}(a_{B_1}(x))) → b_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
A_{B_1}(B_{b_1}(b_{B_1}(x))) → A_{B_1}(x)
b_{B_1}(B_{b_1}(b_{A_1}(x))) → b_{A_1}(x)
b_{B_1}(B_{b_1}(b_{b_1}(x))) → b_{b_1}(x)
b_{B_1}(B_{b_1}(b_{a_1}(x))) → b_{a_1}(x)
b_{B_1}(B_{b_1}(b_{B_1}(x))) → b_{B_1}(x)
a_{B_1}(B_{b_1}(b_{B_1}(x))) → a_{B_1}(x)
B_{B_1}(B_{b_1}(b_{B_1}(x))) → B_{B_1}(x)


(8) Obligation:

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

A_{A_1}(A_{b_1}(b_{A_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
A_{A_1}(A_{b_1}(b_{b_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
A_{A_1}(A_{b_1}(b_{a_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
b_{A_1}(A_{b_1}(b_{A_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
b_{A_1}(A_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
b_{A_1}(A_{b_1}(b_{a_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
B_{A_1}(A_{b_1}(b_{A_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
B_{A_1}(A_{b_1}(b_{b_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
B_{A_1}(A_{b_1}(b_{a_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
A_{B_1}(B_{a_1}(a_{b_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
A_{B_1}(B_{a_1}(a_{a_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
A_{B_1}(B_{a_1}(a_{B_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
a_{B_1}(B_{a_1}(a_{b_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
a_{B_1}(B_{a_1}(a_{a_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
a_{B_1}(B_{a_1}(a_{B_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
B_{B_1}(B_{a_1}(a_{b_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
B_{B_1}(B_{a_1}(a_{a_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
B_{B_1}(B_{a_1}(a_{B_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
A_{A_1}(A_{a_1}(a_{b_1}(x))) → A_{b_1}(x)
b_{A_1}(A_{a_1}(a_{b_1}(x))) → b_{b_1}(x)
B_{A_1}(A_{a_1}(a_{b_1}(x))) → B_{b_1}(x)
B_{A_1}(A_{a_1}(a_{a_1}(x))) → B_{a_1}(x)
B_{A_1}(A_{a_1}(a_{B_1}(x))) → B_{B_1}(x)
A_{B_1}(B_{b_1}(b_{A_1}(x))) → A_{A_1}(x)
A_{B_1}(B_{b_1}(b_{b_1}(x))) → A_{b_1}(x)
A_{B_1}(B_{b_1}(b_{a_1}(x))) → A_{a_1}(x)
a_{B_1}(B_{b_1}(b_{a_1}(x))) → a_{a_1}(x)
B_{B_1}(B_{b_1}(b_{a_1}(x))) → B_{a_1}(x)

Q is empty.

(9) DependencyPairsProof (EQUIVALENT transformation)

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

(10) Obligation:

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

A_{A_1}1(A_{b_1}(b_{A_1}(x))) → A_{B_1}1(B_{A_1}(A_{A_1}(x)))
A_{A_1}1(A_{b_1}(b_{A_1}(x))) → B_{A_1}1(A_{A_1}(x))
A_{A_1}1(A_{b_1}(b_{A_1}(x))) → A_{A_1}1(x)
A_{A_1}1(A_{b_1}(b_{b_1}(x))) → A_{B_1}1(B_{A_1}(A_{b_1}(x)))
A_{A_1}1(A_{b_1}(b_{b_1}(x))) → B_{A_1}1(A_{b_1}(x))
A_{A_1}1(A_{b_1}(b_{a_1}(x))) → A_{B_1}1(B_{A_1}(A_{a_1}(x)))
A_{A_1}1(A_{b_1}(b_{a_1}(x))) → B_{A_1}1(A_{a_1}(x))
B_{A_1}2(A_{b_1}(b_{A_1}(x))) → A_{B_1}1(B_{A_1}(A_{A_1}(x)))
B_{A_1}2(A_{b_1}(b_{A_1}(x))) → B_{A_1}1(A_{A_1}(x))
B_{A_1}2(A_{b_1}(b_{A_1}(x))) → A_{A_1}1(x)
B_{A_1}2(A_{b_1}(b_{b_1}(x))) → A_{B_1}1(B_{A_1}(A_{b_1}(x)))
B_{A_1}2(A_{b_1}(b_{b_1}(x))) → B_{A_1}1(A_{b_1}(x))
B_{A_1}2(A_{b_1}(b_{a_1}(x))) → A_{B_1}1(B_{A_1}(A_{a_1}(x)))
B_{A_1}2(A_{b_1}(b_{a_1}(x))) → B_{A_1}1(A_{a_1}(x))
B_{A_1}1(A_{b_1}(b_{A_1}(x))) → A_{B_1}1(B_{A_1}(A_{A_1}(x)))
B_{A_1}1(A_{b_1}(b_{A_1}(x))) → B_{A_1}1(A_{A_1}(x))
B_{A_1}1(A_{b_1}(b_{A_1}(x))) → A_{A_1}1(x)
B_{A_1}1(A_{b_1}(b_{b_1}(x))) → A_{B_1}1(B_{A_1}(A_{b_1}(x)))
B_{A_1}1(A_{b_1}(b_{b_1}(x))) → B_{A_1}1(A_{b_1}(x))
B_{A_1}1(A_{b_1}(b_{a_1}(x))) → A_{B_1}1(B_{A_1}(A_{a_1}(x)))
B_{A_1}1(A_{b_1}(b_{a_1}(x))) → B_{A_1}1(A_{a_1}(x))
A_{B_1}2(B_{a_1}(a_{b_1}(x))) → B_{A_1}2(A_{B_1}(B_{b_1}(x)))
A_{B_1}2(B_{a_1}(a_{b_1}(x))) → A_{B_1}2(B_{b_1}(x))
A_{B_1}2(B_{a_1}(a_{a_1}(x))) → B_{A_1}2(A_{B_1}(B_{a_1}(x)))
A_{B_1}2(B_{a_1}(a_{a_1}(x))) → A_{B_1}2(B_{a_1}(x))
A_{B_1}2(B_{a_1}(a_{B_1}(x))) → B_{A_1}2(A_{B_1}(B_{B_1}(x)))
A_{B_1}2(B_{a_1}(a_{B_1}(x))) → A_{B_1}2(B_{B_1}(x))
A_{B_1}2(B_{a_1}(a_{B_1}(x))) → B_{B_1}1(x)
A_{B_1}1(B_{a_1}(a_{b_1}(x))) → B_{A_1}2(A_{B_1}(B_{b_1}(x)))
A_{B_1}1(B_{a_1}(a_{b_1}(x))) → A_{B_1}2(B_{b_1}(x))
A_{B_1}1(B_{a_1}(a_{a_1}(x))) → B_{A_1}2(A_{B_1}(B_{a_1}(x)))
A_{B_1}1(B_{a_1}(a_{a_1}(x))) → A_{B_1}2(B_{a_1}(x))
A_{B_1}1(B_{a_1}(a_{B_1}(x))) → B_{A_1}2(A_{B_1}(B_{B_1}(x)))
A_{B_1}1(B_{a_1}(a_{B_1}(x))) → A_{B_1}2(B_{B_1}(x))
A_{B_1}1(B_{a_1}(a_{B_1}(x))) → B_{B_1}1(x)
B_{B_1}1(B_{a_1}(a_{b_1}(x))) → B_{A_1}2(A_{B_1}(B_{b_1}(x)))
B_{B_1}1(B_{a_1}(a_{b_1}(x))) → A_{B_1}2(B_{b_1}(x))
B_{B_1}1(B_{a_1}(a_{a_1}(x))) → B_{A_1}2(A_{B_1}(B_{a_1}(x)))
B_{B_1}1(B_{a_1}(a_{a_1}(x))) → A_{B_1}2(B_{a_1}(x))
B_{B_1}1(B_{a_1}(a_{B_1}(x))) → B_{A_1}2(A_{B_1}(B_{B_1}(x)))
B_{B_1}1(B_{a_1}(a_{B_1}(x))) → A_{B_1}2(B_{B_1}(x))
B_{B_1}1(B_{a_1}(a_{B_1}(x))) → B_{B_1}1(x)
B_{A_1}1(A_{a_1}(a_{B_1}(x))) → B_{B_1}1(x)
A_{B_1}2(B_{b_1}(b_{A_1}(x))) → A_{A_1}1(x)

The TRS R consists of the following rules:

A_{A_1}(A_{b_1}(b_{A_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
A_{A_1}(A_{b_1}(b_{b_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
A_{A_1}(A_{b_1}(b_{a_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
b_{A_1}(A_{b_1}(b_{A_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
b_{A_1}(A_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
b_{A_1}(A_{b_1}(b_{a_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
B_{A_1}(A_{b_1}(b_{A_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
B_{A_1}(A_{b_1}(b_{b_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
B_{A_1}(A_{b_1}(b_{a_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
A_{B_1}(B_{a_1}(a_{b_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
A_{B_1}(B_{a_1}(a_{a_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
A_{B_1}(B_{a_1}(a_{B_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
a_{B_1}(B_{a_1}(a_{b_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
a_{B_1}(B_{a_1}(a_{a_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
a_{B_1}(B_{a_1}(a_{B_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
B_{B_1}(B_{a_1}(a_{b_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
B_{B_1}(B_{a_1}(a_{a_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
B_{B_1}(B_{a_1}(a_{B_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
A_{A_1}(A_{a_1}(a_{b_1}(x))) → A_{b_1}(x)
b_{A_1}(A_{a_1}(a_{b_1}(x))) → b_{b_1}(x)
B_{A_1}(A_{a_1}(a_{b_1}(x))) → B_{b_1}(x)
B_{A_1}(A_{a_1}(a_{a_1}(x))) → B_{a_1}(x)
B_{A_1}(A_{a_1}(a_{B_1}(x))) → B_{B_1}(x)
A_{B_1}(B_{b_1}(b_{A_1}(x))) → A_{A_1}(x)
A_{B_1}(B_{b_1}(b_{b_1}(x))) → A_{b_1}(x)
A_{B_1}(B_{b_1}(b_{a_1}(x))) → A_{a_1}(x)
a_{B_1}(B_{b_1}(b_{a_1}(x))) → a_{a_1}(x)
B_{B_1}(B_{b_1}(b_{a_1}(x))) → B_{a_1}(x)

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

(11) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].


The following pairs can be oriented strictly and are deleted.


A_{A_1}1(A_{b_1}(b_{A_1}(x))) → B_{A_1}1(A_{A_1}(x))
A_{A_1}1(A_{b_1}(b_{A_1}(x))) → A_{A_1}1(x)
A_{A_1}1(A_{b_1}(b_{b_1}(x))) → B_{A_1}1(A_{b_1}(x))
A_{A_1}1(A_{b_1}(b_{a_1}(x))) → B_{A_1}1(A_{a_1}(x))
B_{A_1}2(A_{b_1}(b_{A_1}(x))) → B_{A_1}1(A_{A_1}(x))
B_{A_1}2(A_{b_1}(b_{A_1}(x))) → A_{A_1}1(x)
B_{A_1}2(A_{b_1}(b_{b_1}(x))) → B_{A_1}1(A_{b_1}(x))
B_{A_1}2(A_{b_1}(b_{a_1}(x))) → B_{A_1}1(A_{a_1}(x))
B_{A_1}1(A_{b_1}(b_{A_1}(x))) → B_{A_1}1(A_{A_1}(x))
B_{A_1}1(A_{b_1}(b_{A_1}(x))) → A_{A_1}1(x)
B_{A_1}1(A_{b_1}(b_{b_1}(x))) → B_{A_1}1(A_{b_1}(x))
B_{A_1}1(A_{b_1}(b_{a_1}(x))) → B_{A_1}1(A_{a_1}(x))
A_{B_1}2(B_{a_1}(a_{b_1}(x))) → B_{A_1}2(A_{B_1}(B_{b_1}(x)))
A_{B_1}2(B_{a_1}(a_{b_1}(x))) → A_{B_1}2(B_{b_1}(x))
A_{B_1}2(B_{a_1}(a_{a_1}(x))) → B_{A_1}2(A_{B_1}(B_{a_1}(x)))
A_{B_1}2(B_{a_1}(a_{a_1}(x))) → A_{B_1}2(B_{a_1}(x))
A_{B_1}2(B_{a_1}(a_{B_1}(x))) → B_{A_1}2(A_{B_1}(B_{B_1}(x)))
A_{B_1}2(B_{a_1}(a_{B_1}(x))) → A_{B_1}2(B_{B_1}(x))
A_{B_1}2(B_{a_1}(a_{B_1}(x))) → B_{B_1}1(x)
A_{B_1}1(B_{a_1}(a_{b_1}(x))) → B_{A_1}2(A_{B_1}(B_{b_1}(x)))
A_{B_1}1(B_{a_1}(a_{b_1}(x))) → A_{B_1}2(B_{b_1}(x))
A_{B_1}1(B_{a_1}(a_{a_1}(x))) → B_{A_1}2(A_{B_1}(B_{a_1}(x)))
A_{B_1}1(B_{a_1}(a_{a_1}(x))) → A_{B_1}2(B_{a_1}(x))
A_{B_1}1(B_{a_1}(a_{B_1}(x))) → B_{A_1}2(A_{B_1}(B_{B_1}(x)))
A_{B_1}1(B_{a_1}(a_{B_1}(x))) → A_{B_1}2(B_{B_1}(x))
A_{B_1}1(B_{a_1}(a_{B_1}(x))) → B_{B_1}1(x)
B_{B_1}1(B_{a_1}(a_{b_1}(x))) → B_{A_1}2(A_{B_1}(B_{b_1}(x)))
B_{B_1}1(B_{a_1}(a_{b_1}(x))) → A_{B_1}2(B_{b_1}(x))
B_{B_1}1(B_{a_1}(a_{a_1}(x))) → B_{A_1}2(A_{B_1}(B_{a_1}(x)))
B_{B_1}1(B_{a_1}(a_{a_1}(x))) → A_{B_1}2(B_{a_1}(x))
B_{B_1}1(B_{a_1}(a_{B_1}(x))) → B_{A_1}2(A_{B_1}(B_{B_1}(x)))
B_{B_1}1(B_{a_1}(a_{B_1}(x))) → A_{B_1}2(B_{B_1}(x))
B_{B_1}1(B_{a_1}(a_{B_1}(x))) → B_{B_1}1(x)
B_{A_1}1(A_{a_1}(a_{B_1}(x))) → B_{B_1}1(x)
A_{B_1}2(B_{b_1}(b_{A_1}(x))) → A_{A_1}1(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(A_{A_1}(x1)) = 1 + x1   
POL(A_{A_1}1(x1)) = x1   
POL(A_{B_1}(x1)) = x1   
POL(A_{B_1}1(x1)) = 1 + x1   
POL(A_{B_1}2(x1)) = x1   
POL(A_{a_1}(x1)) = x1   
POL(A_{b_1}(x1)) = 1 + x1   
POL(B_{A_1}(x1)) = x1   
POL(B_{A_1}1(x1)) = x1   
POL(B_{A_1}2(x1)) = x1   
POL(B_{B_1}(x1)) = 1 + x1   
POL(B_{B_1}1(x1)) = x1   
POL(B_{a_1}(x1)) = 1 + x1   
POL(B_{b_1}(x1)) = x1   
POL(a_{B_1}(x1)) = 1 + x1   
POL(a_{a_1}(x1)) = 1 + x1   
POL(a_{b_1}(x1)) = x1   
POL(b_{A_1}(x1)) = 1 + x1   
POL(b_{a_1}(x1)) = x1   
POL(b_{b_1}(x1)) = 1 + x1   

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

A_{A_1}(A_{b_1}(b_{A_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
A_{A_1}(A_{b_1}(b_{b_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
A_{A_1}(A_{b_1}(b_{a_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
A_{A_1}(A_{a_1}(a_{b_1}(x))) → A_{b_1}(x)
B_{A_1}(A_{b_1}(b_{A_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
B_{A_1}(A_{b_1}(b_{b_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
B_{A_1}(A_{b_1}(b_{a_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
B_{A_1}(A_{a_1}(a_{b_1}(x))) → B_{b_1}(x)
B_{A_1}(A_{a_1}(a_{a_1}(x))) → B_{a_1}(x)
B_{A_1}(A_{a_1}(a_{B_1}(x))) → B_{B_1}(x)
A_{B_1}(B_{b_1}(b_{A_1}(x))) → A_{A_1}(x)
A_{B_1}(B_{b_1}(b_{b_1}(x))) → A_{b_1}(x)
A_{B_1}(B_{b_1}(b_{a_1}(x))) → A_{a_1}(x)
A_{B_1}(B_{a_1}(a_{b_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
A_{B_1}(B_{a_1}(a_{a_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
A_{B_1}(B_{a_1}(a_{B_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
B_{B_1}(B_{a_1}(a_{b_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
B_{B_1}(B_{a_1}(a_{a_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
B_{B_1}(B_{a_1}(a_{B_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
B_{B_1}(B_{b_1}(b_{a_1}(x))) → B_{a_1}(x)
a_{B_1}(B_{a_1}(a_{b_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
a_{B_1}(B_{a_1}(a_{a_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
a_{B_1}(B_{a_1}(a_{B_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
b_{A_1}(A_{b_1}(b_{A_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
b_{A_1}(A_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
b_{A_1}(A_{b_1}(b_{a_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
a_{B_1}(B_{b_1}(b_{a_1}(x))) → a_{a_1}(x)
b_{A_1}(A_{a_1}(a_{b_1}(x))) → b_{b_1}(x)

(12) Obligation:

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

A_{A_1}1(A_{b_1}(b_{A_1}(x))) → A_{B_1}1(B_{A_1}(A_{A_1}(x)))
A_{A_1}1(A_{b_1}(b_{b_1}(x))) → A_{B_1}1(B_{A_1}(A_{b_1}(x)))
A_{A_1}1(A_{b_1}(b_{a_1}(x))) → A_{B_1}1(B_{A_1}(A_{a_1}(x)))
B_{A_1}2(A_{b_1}(b_{A_1}(x))) → A_{B_1}1(B_{A_1}(A_{A_1}(x)))
B_{A_1}2(A_{b_1}(b_{b_1}(x))) → A_{B_1}1(B_{A_1}(A_{b_1}(x)))
B_{A_1}2(A_{b_1}(b_{a_1}(x))) → A_{B_1}1(B_{A_1}(A_{a_1}(x)))
B_{A_1}1(A_{b_1}(b_{A_1}(x))) → A_{B_1}1(B_{A_1}(A_{A_1}(x)))
B_{A_1}1(A_{b_1}(b_{b_1}(x))) → A_{B_1}1(B_{A_1}(A_{b_1}(x)))
B_{A_1}1(A_{b_1}(b_{a_1}(x))) → A_{B_1}1(B_{A_1}(A_{a_1}(x)))

The TRS R consists of the following rules:

A_{A_1}(A_{b_1}(b_{A_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
A_{A_1}(A_{b_1}(b_{b_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
A_{A_1}(A_{b_1}(b_{a_1}(x))) → A_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
b_{A_1}(A_{b_1}(b_{A_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
b_{A_1}(A_{b_1}(b_{b_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
b_{A_1}(A_{b_1}(b_{a_1}(x))) → b_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
B_{A_1}(A_{b_1}(b_{A_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{A_1}(x)))))
B_{A_1}(A_{b_1}(b_{b_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{b_1}(x)))))
B_{A_1}(A_{b_1}(b_{a_1}(x))) → B_{b_1}(b_{a_1}(a_{B_1}(B_{A_1}(A_{a_1}(x)))))
A_{B_1}(B_{a_1}(a_{b_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
A_{B_1}(B_{a_1}(a_{a_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
A_{B_1}(B_{a_1}(a_{B_1}(x))) → A_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
a_{B_1}(B_{a_1}(a_{b_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
a_{B_1}(B_{a_1}(a_{a_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
a_{B_1}(B_{a_1}(a_{B_1}(x))) → a_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
B_{B_1}(B_{a_1}(a_{b_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{b_1}(x)))))
B_{B_1}(B_{a_1}(a_{a_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{a_1}(x)))))
B_{B_1}(B_{a_1}(a_{B_1}(x))) → B_{a_1}(a_{b_1}(b_{A_1}(A_{B_1}(B_{B_1}(x)))))
A_{A_1}(A_{a_1}(a_{b_1}(x))) → A_{b_1}(x)
b_{A_1}(A_{a_1}(a_{b_1}(x))) → b_{b_1}(x)
B_{A_1}(A_{a_1}(a_{b_1}(x))) → B_{b_1}(x)
B_{A_1}(A_{a_1}(a_{a_1}(x))) → B_{a_1}(x)
B_{A_1}(A_{a_1}(a_{B_1}(x))) → B_{B_1}(x)
A_{B_1}(B_{b_1}(b_{A_1}(x))) → A_{A_1}(x)
A_{B_1}(B_{b_1}(b_{b_1}(x))) → A_{b_1}(x)
A_{B_1}(B_{b_1}(b_{a_1}(x))) → A_{a_1}(x)
a_{B_1}(B_{b_1}(b_{a_1}(x))) → a_{a_1}(x)
B_{B_1}(B_{b_1}(b_{a_1}(x))) → B_{a_1}(x)

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

(13) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 9 less nodes.

(14) TRUE