(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3. This implies Q-termination of R.
The following rules were used to construct the certificate:
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(X))
mark(a) → active(a)
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
8214219, 8214220, 8214224, 8214222, 8214223, 8214221, 8214225, 8214226, 8214227, 8214228, 8214229, 8214232, 8214233, 8214230, 8214231, 8214234
Node 8214219 is start node and node 8214220 is final node.
Those nodes are connect through the following edges:
- 8214219 to 8214220 labelled g_1(0), f_1(0), f_1(1), g_1(1)
- 8214219 to 8214221 labelled mark_1(0)
- 8214219 to 8214225 labelled active_1(0)
- 8214219 to 8214219 labelled active_1(0)
- 8214219 to 8214224 labelled active_1(0)
- 8214219 to 8214227 labelled active_1(1)
- 8214219 to 8214230 labelled mark_1(1)
- 8214219 to 8214234 labelled active_1(2)
- 8214220 to 8214220 labelled #_1(0)
- 8214224 to 8214220 labelled a(0)
- 8214222 to 8214223 labelled g_1(0)
- 8214223 to 8214224 labelled f_1(0)
- 8214221 to 8214222 labelled f_1(0)
- 8214225 to 8214226 labelled g_1(0)
- 8214225 to 8214220 labelled g_1(1)
- 8214225 to 8214228 labelled g_1(1)
- 8214225 to 8214219 labelled g_1(1)
- 8214225 to 8214224 labelled g_1(1)
- 8214225 to 8214225 labelled g_1(1)
- 8214225 to 8214230 labelled g_1(1), g_1(2)
- 8214225 to 8214227 labelled g_1(2)
- 8214225 to 8214234 labelled g_1(2), g_1(1)
- 8214225 to 8214221 labelled g_1(1)
- 8214226 to 8214220 labelled mark_1(0)
- 8214226 to 8214228 labelled active_1(1)
- 8214226 to 8214219 labelled active_1(1)
- 8214226 to 8214230 labelled mark_1(1)
- 8214226 to 8214234 labelled active_1(2)
- 8214227 to 8214222 labelled f_1(1)
- 8214228 to 8214229 labelled g_1(1)
- 8214228 to 8214220 labelled a(1), g_1(2), g_1(1)
- 8214228 to 8214228 labelled g_1(2)
- 8214228 to 8214219 labelled g_1(2), g_1(1)
- 8214228 to 8214230 labelled g_1(2)
- 8214228 to 8214224 labelled g_1(1)
- 8214228 to 8214225 labelled g_1(1)
- 8214228 to 8214227 labelled g_1(2)
- 8214228 to 8214221 labelled g_1(1)
- 8214228 to 8214234 labelled g_1(3), g_1(2)
- 8214229 to 8214220 labelled mark_1(1)
- 8214229 to 8214228 labelled active_1(1)
- 8214229 to 8214219 labelled active_1(1)
- 8214229 to 8214230 labelled mark_1(1)
- 8214229 to 8214234 labelled active_1(2)
- 8214232 to 8214233 labelled f_1(1)
- 8214233 to 8214220 labelled a(1)
- 8214230 to 8214231 labelled f_1(1)
- 8214231 to 8214232 labelled g_1(1)
- 8214234 to 8214231 labelled f_1(2)