Termination w.r.t. Q proof of /tmp/tmplUaNcK/z008.srs

Termination w.r.t. Q of the following Term Rewriting System could be proven:

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

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

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

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

The set Q is empty.
We have obtained the following QTRS:

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

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

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

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

Q is empty.

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

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
The following rules can be removed by the rule removal processor [15] because they are oriented strictly by a polynomial ordering:

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))

Used ordering:
Polynomial interpretation [25]:

POL(a(x₁)) = 2·x₁
POL(b(x₁)) = 2·x₁
POL(s(x₁)) = 2 + 2·x₁

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

  ↳ QTRS Reverse

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

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.

Using Dependency Pairs [1,15] we result in the following initial DP problem:
Q DP problem:
The TRS P consists of the following rules:

A(b(a(a(x1)))) → B(a(x1))
A(b(a(a(x1)))) → A(b(a(x1)))
B(a(b(b(x1)))) → A(b(x1))
A(b(a(a(x1)))) → B(a(b(a(x1))))
B(a(b(b(x1)))) → B(a(b(x1)))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

  ↳ QTRS Reverse

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

A(b(a(a(x1)))) → B(a(x1))
A(b(a(a(x1)))) → A(b(a(x1)))
B(a(b(b(x1)))) → A(b(x1))
A(b(a(a(x1)))) → B(a(b(a(x1))))
B(a(b(b(x1)))) → B(a(b(x1)))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the rule removal processor [15] with the following polynomial ordering [25], at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:

A(b(a(a(x1)))) → B(a(x1))
A(b(a(a(x1)))) → A(b(a(x1)))
B(a(b(b(x1)))) → A(b(x1))
B(a(b(b(x1)))) → B(a(b(x1)))

Used ordering: POLO with Polynomial interpretation [25]:

POL(A(x₁)) = x₁
POL(B(x₁)) = x₁
POL(a(x₁)) = 2 + 2·x₁
POL(b(x₁)) = 2 + 2·x₁

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

  ↳ QTRS Reverse

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

A(b(a(a(x1)))) → B(a(b(a(x1))))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule A(b(a(a(x1)))) → B(a(b(a(x1)))) at position [0] we obtained the following new rules:

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

  ↳ QTRS Reverse

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

A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(x1)))) → A(b(a(b(x1))))

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By narrowing [15] the rule B(a(b(b(x1)))) → A(b(a(b(x1)))) at position [0] we obtained the following new rules:

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ QDPToSRSProof

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The finiteness of this DP problem is implied by strong termination of a SRS due to [12].

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ QDPToSRSProof

                        ↳ QTRS

                          ↳ QTRS Reverse

  ↳ QTRS Reverse

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

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))
B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))

Q is empty.

We have reversed the following QTRS:
The set of rules R is

b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))
B(a(b(b(a(b(b(x0))))))) → A(b(a(a(b(a(b(x0)))))))
A(b(a(a(b(a(a(x0))))))) → B(a(b(b(a(b(a(x0)))))))
A(b(a(a(a(x0))))) → B(b(a(b(a(x0)))))
A(b(a(a(b(b(x0)))))) → B(a(a(b(a(b(x0))))))
B(a(b(b(a(a(x0)))))) → A(b(b(a(b(a(x0))))))
B(a(b(b(b(x0))))) → A(a(b(a(b(x0)))))

The set Q is empty.
We have obtained the following QTRS:

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

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

    ↳ QTRS

      ↳ DependencyPairsProof

        ↳ QDP

          ↳ RuleRemovalProof

            ↳ QDP

              ↳ Narrowing

                ↳ QDP

                  ↳ Narrowing

                    ↳ QDP

                      ↳ QDPToSRSProof

                        ↳ QTRS

                          ↳ QTRS Reverse

                            ↳ QTRS

                              ↳ RFCMatchBoundsTRSProof

  ↳ QTRS Reverse

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

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

Q is empty.

Termination of the TRS R could be shown with a Match Bound [6,7] of 1. This implies Q-termination of R.
The following rules were used to construct the certificate:

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

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

532, 533, 537, 536, 534, 535, 542, 539, 540, 538, 541, 547, 548, 544, 545, 543, 546, 554, 552, 553, 551, 549, 550, 558, 557, 555, 556, 564, 562, 563, 561, 559, 560, 569, 566, 567, 565, 568, 574, 575, 571, 572, 570, 573

Node 532 is start node and node 533 is final node.

Those nodes are connect through the following edges:

532 to 534 labelled b_1(0)
532 to 538 labelled a_1(0)
532 to 543 labelled a_1(0)
532 to 549 labelled b_1(0)
533 to 533 labelled #_1(0)
537 to 533 labelled A_1(0)
536 to 537 labelled a_1(0)
536 to 533 labelled a_1(0)
536 to 565 labelled a_1(1)
536 to 570 labelled a_1(1)
534 to 535 labelled a_1(0)
535 to 536 labelled b_1(0)
542 to 533 labelled A_1(0)
539 to 540 labelled a_1(0)
540 to 541 labelled b_1(0)
538 to 539 labelled b_1(0)
541 to 542 labelled b_1(0)
547 to 548 labelled a_1(0)
548 to 533 labelled B_1(0)
544 to 545 labelled a_1(0)
545 to 546 labelled b_1(0)
545 to 533 labelled b_1(0)
545 to 555 labelled b_1(1)
545 to 559 labelled b_1(1)
543 to 544 labelled b_1(0)
546 to 547 labelled b_1(0)
546 to 533 labelled B_1(0)
554 to 533 labelled A_1(0)
552 to 553 labelled a_1(0)
553 to 554 labelled b_1(0)
553 to 533 labelled B_1(0)
551 to 552 labelled a_1(0)
549 to 550 labelled a_1(0)
550 to 551 labelled b_1(0)
558 to 533 labelled A_1(1)
557 to 558 labelled a_1(1)
557 to 533 labelled a_1(1)
557 to 565 labelled a_1(1)
557 to 570 labelled a_1(1)
555 to 556 labelled a_1(1)
556 to 557 labelled b_1(1)
564 to 533 labelled A_1(1)
562 to 563 labelled a_1(1)
563 to 564 labelled b_1(1)
563 to 533 labelled B_1(1)
561 to 562 labelled a_1(1)
559 to 560 labelled a_1(1)
560 to 561 labelled b_1(1)
569 to 533 labelled A_1(1)
566 to 567 labelled a_1(1)
567 to 568 labelled b_1(1)
567 to 533 labelled b_1(1)
567 to 555 labelled b_1(1)
567 to 559 labelled b_1(1)
565 to 566 labelled b_1(1)
568 to 569 labelled b_1(1)
568 to 533 labelled B_1(1)
574 to 575 labelled a_1(1)
575 to 533 labelled B_1(1)
571 to 572 labelled a_1(1)
572 to 573 labelled b_1(1)
570 to 571 labelled b_1(1)
573 to 574 labelled b_1(1)

We have reversed the following QTRS:
The set of rules R is

a(s(x1)) → s(a(x1))
b(a(b(s(x1)))) → a(b(s(a(x1))))
b(a(b(b(x1)))) → a(b(a(b(x1))))
a(b(a(a(x1)))) → b(a(b(a(x1))))

The set Q is empty.
We have obtained the following QTRS:

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

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ RRRPoloQTRSProof

  ↳ QTRS Reverse

    ↳ QTRS

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

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

Q is empty.