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

Q is empty.


QTRS
  ↳ RFCMatchBoundsTRSProof

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

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

Q is empty.

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

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

The certificate found is represented by the following graph.

The certificate consists of the following enumerated nodes:

1, 2, 4, 5, 3, 9, 8, 7, 6, 11, 12, 10, 16, 15, 14, 13, 18, 19, 17, 23, 22, 21, 20, 25, 26, 24, 30, 29, 28, 27, 32, 33, 31, 37, 36, 35, 34, 39, 40, 38, 44, 43, 42, 41, 46, 47, 45, 51, 50, 49, 48, 58, 59, 57, 63, 62, 61, 60, 65, 66, 64, 70, 69, 68, 67, 72, 73, 71, 77, 76, 75, 74, 79, 80, 78, 84, 83, 82, 81

Node 1 is start node and node 2 is final node.

Those nodes are connect through the following edges: