(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:
f(f(x)) → f(x)
f(s(x)) → f(x)
g(s(0)) → g(f(s(0)))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
9412464, 9412465, 9412466, 9412468, 9412467
Node 9412464 is start node and node 9412465 is final node.
Those nodes are connect through the following edges:
- 9412464 to 9412465 labelled f_1(0), f_1(1)
- 9412464 to 9412466 labelled g_1(0)
- 9412465 to 9412465 labelled #_1(0)
- 9412466 to 9412467 labelled f_1(0)
- 9412466 to 9412468 labelled f_1(1)
- 9412468 to 9412465 labelled 0(0)
- 9412467 to 9412468 labelled s_1(0)