(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 5. 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:
8444735, 8444736, 8444737, 8444738, 8444739, 8444740, 8444741, 8444742, 8444743, 8444744
Node 8444735 is start node and node 8444736 is final node.
Those nodes are connect through the following edges:
- 8444735 to 8444736 labelled h_1(0), g_1(0), h_1(1), g_1(1)
- 8444735 to 8444737 labelled active_1(0), mark_1(0)
- 8444735 to 8444735 labelled active_1(0), mark_1(0), active_1(1), mark_1(1)
- 8444735 to 8444738 labelled active_1(1), mark_1(1)
- 8444735 to 8444739 labelled mark_1(2), active_1(2)
- 8444735 to 8444740 labelled active_1(2)
- 8444735 to 8444741 labelled active_1(3)
- 8444735 to 8444742 labelled mark_1(3), active_1(3)
- 8444735 to 8444743 labelled active_1(4), mark_1(4)
- 8444735 to 8444744 labelled active_1(5)
- 8444736 to 8444736 labelled #_1(0), c(0), c(1)
- 8444737 to 8444736 labelled c(0), d(0)
- 8444738 to 8444736 labelled d(1), c(1), h_1(1), g_1(1)
- 8444739 to 8444736 labelled h_1(2), d(2), c(2), h_1(1)
- 8444740 to 8444736 labelled g_1(2), g_1(1)
- 8444741 to 8444736 labelled c(3)
- 8444742 to 8444736 labelled d(3), h_1(3), h_1(1)
- 8444743 to 8444736 labelled d(4), h_1(4), h_1(1)
- 8444744 to 8444736 labelled d(5), h_1(5), h_1(1)