(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 0. This implies Q-termination of R.
The following rules were used to construct the certificate:
f(a) → f(b)
g(b) → g(a)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
9111257, 9111258, 9111259, 9111260
Node 9111257 is start node and node 9111258 is final node.
Those nodes are connect through the following edges:
- 9111257 to 9111259 labelled g_1(0)
- 9111257 to 9111260 labelled f_1(0)
- 9111258 to 9111258 labelled #_1(0)
- 9111259 to 9111258 labelled a(0)
- 9111260 to 9111258 labelled b(0)