(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:
262705, 262706, 262707, 262708, 262709, 262710, 262711, 262712
Node 262705 is start node and node 262706 is final node.
Those nodes are connect through the following edges:
- 262705 to 262706 labelled h_1(0), g_1(0), g_1(1), h_1(1)
- 262705 to 262707 labelled active_1(0), mark_1(0)
- 262705 to 262705 labelled active_1(0), mark_1(0), active_1(1), mark_1(1)
- 262705 to 262708 labelled active_1(1), mark_1(1)
- 262705 to 262709 labelled active_1(2)
- 262705 to 262710 labelled mark_1(2), active_1(2)
- 262705 to 262711 labelled mark_1(3), active_1(3)
- 262705 to 262712 labelled active_1(4)
- 262706 to 262706 labelled #_1(0), c(0), c(1)
- 262707 to 262706 labelled c(0), d(0)
- 262708 to 262706 labelled d(1), c(1)
- 262709 to 262706 labelled c(2), g_1(2), g_1(1)
- 262710 to 262706 labelled d(2), h_1(2), h_1(1)
- 262711 to 262706 labelled h_1(3), d(3), h_1(1)
- 262712 to 262706 labelled h_1(4), d(4), h_1(1)