Termination w.r.t. Q proof of /tmp/tmpdTG1vF/z024.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(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(x1)))

Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

a(b(a(x1))) → a(a(b(b(a(a(x1))))))
b(a(a(b(x1)))) → b(a(b(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(x1))) → B(b(a(a(x1))))
A(b(a(x1))) → A(a(b(b(a(a(x1))))))
B(a(a(b(x1)))) → B(a(b(x1)))
A(b(a(x1))) → A(b(b(a(a(x1)))))
A(b(a(x1))) → A(a(x1))
A(b(a(x1))) → B(a(a(x1)))

The TRS R consists of the following rules:

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

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 2 SCCs with 2 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ Narrowing

          ↳ QDP

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

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

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ Narrowing

              ↳ QDP

                ↳ SemLabProof

                ↳ SemLabProof2

          ↳ QDP

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We found the following model for the rules of the TRS R. Interpretation over the domain with elements from 0 to 1.B: 0
a: 0
b: 1
By semantic labelling [33] we obtain the following labelled TRS:Q DP problem:
The TRS P consists of the following rules:

B.0(a.0(a.1(b.0(a.0(a.1(b.0(x0))))))) → B.0(a.1(b.0(a.1(b.0(x0)))))
B.0(a.0(a.1(b.0(a.0(x0))))) → B.0(a.0(a.1(b.1(b.0(a.0(a.0(x0)))))))
B.0(a.0(a.1(b.0(a.0(a.1(b.1(x0))))))) → B.0(a.1(b.0(a.1(b.1(x0)))))
B.0(a.0(a.1(b.0(a.1(x0))))) → B.0(a.0(a.1(b.1(b.0(a.0(a.1(x0)))))))

The TRS R consists of the following rules:

a.1(b.0(a.0(x1))) → a.0(a.1(b.1(b.0(a.0(a.0(x1))))))
a.1(b.0(a.1(x1))) → a.0(a.1(b.1(b.0(a.0(a.1(x1))))))
b.0(a.0(a.1(b.1(x1)))) → b.0(a.1(b.1(x1)))
b.0(a.0(a.1(b.0(x1)))) → b.0(a.1(b.0(x1)))

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ Narrowing

              ↳ QDP

                ↳ SemLabProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                ↳ SemLabProof2

          ↳ QDP

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

B.0(a.0(a.1(b.0(a.0(a.1(b.0(x0))))))) → B.0(a.1(b.0(a.1(b.0(x0)))))
B.0(a.0(a.1(b.0(a.0(x0))))) → B.0(a.0(a.1(b.1(b.0(a.0(a.0(x0)))))))
B.0(a.0(a.1(b.0(a.0(a.1(b.1(x0))))))) → B.0(a.1(b.0(a.1(b.1(x0)))))
B.0(a.0(a.1(b.0(a.1(x0))))) → B.0(a.0(a.1(b.1(b.0(a.0(a.1(x0)))))))

The TRS R consists of the following rules:

a.1(b.0(a.0(x1))) → a.0(a.1(b.1(b.0(a.0(a.0(x1))))))
a.1(b.0(a.1(x1))) → a.0(a.1(b.1(b.0(a.0(a.1(x1))))))
b.0(a.0(a.1(b.1(x1)))) → b.0(a.1(b.1(x1)))
b.0(a.0(a.1(b.0(x1)))) → b.0(a.1(b.0(x1)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph [15,17,22] contains 1 SCC with 2 less nodes.

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ Narrowing

              ↳ QDP

                ↳ SemLabProof

                  ↳ QDP

                    ↳ DependencyGraphProof

                      ↳ QDP

                ↳ SemLabProof2

          ↳ QDP

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

B.0(a.0(a.1(b.0(a.0(a.1(b.0(x0))))))) → B.0(a.1(b.0(a.1(b.0(x0)))))
B.0(a.0(a.1(b.0(a.0(a.1(b.1(x0))))))) → B.0(a.1(b.0(a.1(b.1(x0)))))

The TRS R consists of the following rules:

a.1(b.0(a.0(x1))) → a.0(a.1(b.1(b.0(a.0(a.0(x1))))))
a.1(b.0(a.1(x1))) → a.0(a.1(b.1(b.0(a.0(a.1(x1))))))
b.0(a.0(a.1(b.1(x1)))) → b.0(a.1(b.1(x1)))
b.0(a.0(a.1(b.0(x1)))) → b.0(a.1(b.0(x1)))

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
As can be seen after transforming the QDP problem by semantic labelling [33] and then some rule deleting processors, only certain labelled rules and pairs can be used. Hence, we only have to consider all unlabelled pairs and rules (without the decreasing rules for quasi-models).

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

            ↳ Narrowing

              ↳ QDP

                ↳ SemLabProof

                ↳ SemLabProof2

                  ↳ QDP

                    ↳ RFCMatchBoundsDPProof

          ↳ QDP

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
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:

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

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

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

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

443, 444, 448, 446, 447, 445, 450, 449, 453, 454, 452, 455, 451, 458, 459, 457, 460, 456, 463, 464, 462, 465, 461, 467, 466, 469, 468, 472, 473, 471, 474, 470, 476, 475, 478, 477, 479, 480, 481, 482

Node 443 is start node and node 444 is final node.

Those nodes are connect through the following edges:

443 to 445 labelled B_1(0)
444 to 444 labelled #_1(0)
448 to 444 labelled b_1(0)
448 to 449 labelled b_1(1)
448 to 468 labelled b_1(2)
448 to 461 labelled b_1(2)
446 to 447 labelled b_1(0)
446 to 451 labelled b_1(1)
446 to 456 labelled b_1(1)
447 to 448 labelled a_1(0)
447 to 451 labelled a_1(1)
447 to 456 labelled a_1(1)
445 to 446 labelled a_1(0)
445 to 456 labelled a_1(1)
450 to 444 labelled b_1(1)
450 to 449 labelled b_1(1)
450 to 468 labelled b_1(2)
450 to 461 labelled b_1(2)
449 to 450 labelled a_1(1)
449 to 451 labelled a_1(1)
449 to 461 labelled a_1(2)
453 to 454 labelled b_1(1)
453 to 449 labelled b_1(1)
453 to 468 labelled b_1(2)
453 to 466 labelled b_1(2)
453 to 461 labelled b_1(2)
453 to 477 labelled b_1(3)
453 to 470 labelled b_1(3)
453 to 465 labelled b_1(2)
453 to 479 labelled b_1(4)
454 to 455 labelled a_1(1)
452 to 453 labelled b_1(1)
455 to 444 labelled a_1(1)
455 to 451 labelled a_1(1)
455 to 450 labelled a_1(1)
455 to 461 labelled a_1(2)
451 to 452 labelled a_1(1)
458 to 459 labelled b_1(1)
458 to 466 labelled b_1(2)
458 to 449 labelled b_1(1)
458 to 468 labelled b_1(2)
458 to 461 labelled b_1(2)
458 to 477 labelled b_1(3)
458 to 470 labelled b_1(3)
458 to 479 labelled b_1(4)
459 to 460 labelled a_1(1)
457 to 458 labelled b_1(1)
460 to 448 labelled a_1(1)
460 to 451 labelled a_1(1)
460 to 461 labelled a_1(2), a_1(1)
460 to 469 labelled a_1(1)
460 to 456 labelled a_1(1)
460 to 462 labelled a_1(1)
460 to 457 labelled a_1(1)
456 to 457 labelled a_1(1)
463 to 464 labelled b_1(2)
463 to 466 labelled b_1(2)
463 to 475 labelled b_1(3)
463 to 477 labelled b_1(3)
463 to 468 labelled b_1(2)
463 to 470 labelled b_1(3)
463 to 479 labelled b_1(4)
464 to 465 labelled a_1(2)
462 to 463 labelled b_1(2)
462 to 458 labelled b_1(2)
465 to 450 labelled a_1(2)
465 to 451 labelled a_1(1), a_1(2)
465 to 461 labelled a_1(2)
465 to 470 labelled a_1(3)
461 to 462 labelled a_1(2)
467 to 449 labelled b_1(2), b_1(1)
467 to 468 labelled b_1(2)
467 to 444 labelled b_1(2)
467 to 469 labelled a_1(2)
467 to 477 labelled b_1(3)
467 to 461 labelled b_1(2)
467 to 479 labelled b_1(4)
466 to 467 labelled a_1(2)
466 to 461 labelled a_1(2)
466 to 451 labelled a_1(1)
466 to 470 labelled a_1(3)
469 to 453 labelled b_1(2)
468 to 469 labelled a_1(2)
472 to 473 labelled b_1(3)
472 to 477 labelled b_1(3)
472 to 481 labelled b_1(4)
472 to 479 labelled b_1(4)
473 to 474 labelled a_1(3)
471 to 472 labelled b_1(3)
474 to 469 labelled a_1(3)
474 to 461 labelled a_1(3)
474 to 462 labelled a_1(3)
474 to 478 labelled a_1(3)
474 to 470 labelled a_1(3)
470 to 471 labelled a_1(3)
476 to 468 labelled b_1(3)
475 to 476 labelled a_1(3)
475 to 470 labelled a_1(3)
478 to 463 labelled b_1(3)
478 to 461 labelled b_1(3)
478 to 453 labelled b_1(3)
478 to 458 labelled b_1(3)
478 to 480 labelled a_1(3)
477 to 478 labelled a_1(3)
477 to 470 labelled a_1(3)
479 to 480 labelled a_1(4)
480 to 472 labelled b_1(4)
480 to 458 labelled b_1(4)
481 to 482 labelled a_1(4)
481 to 470 labelled a_1(3)
482 to 463 labelled b_1(4)
482 to 461 labelled b_1(4)
482 to 453 labelled b_1(4)

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.

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

Used ordering: Polynomial Order [21,25] with Interpretation:

POL( A(x₁) ) = x₁

POL( a(x₁) ) = 0

POL( b(x₁) ) = 1

The following usable rules [17] were oriented:

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
We use the reduction pair processor [15].

The following pairs can be oriented strictly and are deleted.

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

The remaining pairs can at least be oriented weakly.
none
Used ordering: Polynomial interpretation [25,35]:

POL(a(x₁)) = 1/4
POL(A(x₁)) = (4)x_1
POL(b(x₁)) = (1/2)x_1

The value of delta used in the strict ordering is 1/4.
The following usable rules [17] were oriented:

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

↳ QTRS

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ AND

          ↳ QDP

          ↳ QDP

            ↳ QDPOrderProof

              ↳ QDP

                ↳ QDPOrderProof

                  ↳ QDP

                    ↳ PisEmptyProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

Q DP problem:
P is empty.
The TRS R consists of the following rules:

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

Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
We have reversed the following QTRS:
The set of rules R is

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

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

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

The set Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ QTRS Reverse

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

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

Q is empty.

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

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

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

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

The set Q is empty.

↳ QTRS

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

  ↳ QTRS Reverse

    ↳ QTRS

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

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

Q is empty.