(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 4. This implies Q-termination of R.
The following rules were used to construct the certificate:
active(g(X)) → mark(h(X))
active(c) → mark(d)
active(h(d)) → mark(g(c))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(X))
mark(c) → active(c)
mark(d) → active(d)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
1882176, 1882177, 1882178, 1882179, 1882180, 1882181, 1882182, 1882183, 1882184
Node 1882176 is start node and node 1882177 is final node.
Those nodes are connect through the following edges:
- 1882176 to 1882177 labelled h_1(0), g_1(0), h_1(1), g_1(1), c(1), active_1(1)
- 1882176 to 1882178 labelled active_1(0), mark_1(0)
- 1882176 to 1882176 labelled active_1(0), mark_1(0), active_1(1), mark_1(1)
- 1882176 to 1882179 labelled active_1(1), mark_1(1)
- 1882176 to 1882180 labelled mark_1(2), active_1(2)
- 1882176 to 1882181 labelled active_1(2)
- 1882176 to 1882182 labelled active_1(3), mark_1(3)
- 1882176 to 1882183 labelled mark_1(3), active_1(3)
- 1882176 to 1882184 labelled active_1(4)
- 1882177 to 1882177 labelled #_1(0), c(0), c(1)
- 1882178 to 1882177 labelled c(0), d(0)
- 1882179 to 1882177 labelled d(1)
- 1882180 to 1882177 labelled d(2), h_1(2), h_1(1)
- 1882181 to 1882177 labelled c(2), g_1(2), g_1(1)
- 1882182 to 1882177 labelled d(3)
- 1882183 to 1882177 labelled h_1(3), h_1(1)
- 1882184 to 1882177 labelled d(4), h_1(4), h_1(1)