Termination w.r.t. Q proof of /tmp/tmp0vm-2r/un12.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:

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

Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

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

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

Q is empty.

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

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

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

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

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

    ↳ QTRS

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

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

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

Q is empty.

We were given the following TRS:

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

By stripping symbols from the only rule of the system, we obtained the following TRS:

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

    ↳ QTRS

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

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

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

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

The TRS R consists of the following rules:

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

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

b(b(b(a(b(a(b(b(a(b(x1)))))))))) → b(b(a(b(a(b(b(b(a(b(a(b(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 1 SCC with 6 less nodes.

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

    ↳ QDP

      ↳ DependencyGraphProof

        ↳ QDP

  ↳ QTRS Reverse

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

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

The TRS R consists of the following rules:

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

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

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

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

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

The set Q is empty.

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

    ↳ QTRS

      ↳ Strip Symbols Proof

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

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

Q is empty.

We were given the following TRS:

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

By stripping symbols from the only rule of the system, we obtained the following TRS:

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

↳ QTRS

  ↳ QTRS Reverse

  ↳ Strip Symbols Proof

  ↳ DependencyPairsProof

  ↳ QTRS Reverse

    ↳ QTRS

      ↳ Strip Symbols Proof

        ↳ QTRS

          ↳ RFCMatchBoundsTRSProof

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

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

Q is empty.

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

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

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

450, 451, 462, 461, 459, 460, 457, 458, 456, 455, 453, 454, 452, 473, 472, 470, 471, 468, 469, 467, 466, 464, 465, 463, 484, 483, 481, 482, 479, 480, 478, 477, 475, 476, 474, 495, 494, 492, 493, 490, 491, 489, 488, 486, 487, 485

Node 450 is start node and node 451 is final node.

Those nodes are connect through the following edges:

450 to 452 labelled b_1(0)
451 to 451 labelled #_1(0)
462 to 451 labelled b_1(0)
461 to 462 labelled b_1(0)
459 to 460 labelled b_1(0)
460 to 461 labelled a_1(0)
460 to 463 labelled b_1(1)
457 to 458 labelled b_1(0)
458 to 459 labelled a_1(0)
458 to 474 labelled b_1(1)
456 to 457 labelled b_1(0)
455 to 456 labelled b_1(0)
453 to 454 labelled b_1(0)
454 to 455 labelled a_1(0)
452 to 453 labelled a_1(0)
473 to 451 labelled b_1(1)
472 to 473 labelled b_1(1)
470 to 471 labelled b_1(1)
471 to 472 labelled a_1(1)
471 to 463 labelled b_1(1)
468 to 469 labelled b_1(1)
469 to 470 labelled a_1(1)
469 to 485 labelled b_1(2)
467 to 468 labelled b_1(1)
466 to 467 labelled b_1(1)
464 to 465 labelled b_1(1)
465 to 466 labelled a_1(1)
463 to 464 labelled a_1(1)
484 to 469 labelled b_1(1)
483 to 484 labelled b_1(1)
481 to 482 labelled b_1(1)
482 to 483 labelled a_1(1)
482 to 463 labelled b_1(1)
479 to 480 labelled b_1(1)
480 to 481 labelled a_1(1)
480 to 485 labelled b_1(2)
478 to 479 labelled b_1(1)
477 to 478 labelled b_1(1)
475 to 476 labelled b_1(1)
476 to 477 labelled a_1(1)
474 to 475 labelled a_1(1)
495 to 469 labelled b_1(2)
494 to 495 labelled b_1(2)
492 to 493 labelled b_1(2)
493 to 494 labelled a_1(2)
493 to 463 labelled b_1(1)
490 to 491 labelled b_1(2)
491 to 492 labelled a_1(2)
491 to 485 labelled b_1(2)
489 to 490 labelled b_1(2)
488 to 489 labelled b_1(2)
486 to 487 labelled b_1(2)
487 to 488 labelled a_1(2)
485 to 486 labelled a_1(2)