(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1. This implies Q-termination of R.
The following rules were used to construct the certificate:
a(a(x)) → a(b(a(x)))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
9114429, 9114430, 9114431, 9114432, 9114433, 9114434
Node 9114429 is start node and node 9114430 is final node.
Those nodes are connect through the following edges:
- 9114429 to 9114431 labelled a_1(0)
- 9114430 to 9114430 labelled #_1(0)
- 9114431 to 9114432 labelled b_1(0)
- 9114432 to 9114430 labelled a_1(0)
- 9114432 to 9114433 labelled a_1(1)
- 9114433 to 9114434 labelled b_1(1)
- 9114434 to 9114430 labelled a_1(1)
- 9114434 to 9114433 labelled a_1(1)