(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(1) → f(g(1))
f(f(x)) → f(x)
g(0) → g(f(0))
g(g(x)) → g(x)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
2928136, 2928137, 2928139, 2928138, 2928141, 2928140, 2928142, 2928143, 2928144, 2928145
Node 2928136 is start node and node 2928137 is final node.
Those nodes are connect through the following edges:
- 2928136 to 2928138 labelled g_1(0)
- 2928136 to 2928140 labelled f_1(0)
- 2928136 to 2928137 labelled f_1(0), g_1(0), f_1(1), g_1(1)
- 2928136 to 2928142 labelled f_1(1)
- 2928136 to 2928144 labelled g_1(1)
- 2928137 to 2928137 labelled #_1(0)
- 2928139 to 2928137 labelled 0(0)
- 2928138 to 2928139 labelled f_1(0)
- 2928141 to 2928137 labelled 1(0)
- 2928140 to 2928141 labelled g_1(0)
- 2928142 to 2928143 labelled g_1(1)
- 2928143 to 2928137 labelled 1(1)
- 2928144 to 2928145 labelled f_1(1)
- 2928145 to 2928137 labelled 0(1)