(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2. This implies Q-termination of R.
The following rules were used to construct the certificate:
a__f(X) → g(h(f(X)))
mark(f(X)) → a__f(mark(X))
mark(g(X)) → g(X)
mark(h(X)) → h(mark(X))
a__f(X) → f(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
7565914, 7565915, 7565916, 7565917, 7565918, 7565920, 7565919, 7565921, 7565923, 7565922
Node 7565914 is start node and node 7565915 is final node.
Those nodes are connect through the following edges:
- 7565914 to 7565915 labelled g_1(0), f_1(0)
- 7565914 to 7565916 labelled a__f_1(0), h_1(0), f_1(1)
- 7565914 to 7565917 labelled g_1(0)
- 7565914 to 7565919 labelled g_1(1)
- 7565915 to 7565915 labelled #_1(0)
- 7565916 to 7565915 labelled mark_1(0), g_1(1)
- 7565916 to 7565921 labelled a__f_1(1), h_1(1), f_1(2)
- 7565916 to 7565922 labelled g_1(2)
- 7565917 to 7565918 labelled h_1(0)
- 7565918 to 7565915 labelled f_1(0)
- 7565920 to 7565916 labelled f_1(1)
- 7565919 to 7565920 labelled h_1(1)
- 7565921 to 7565915 labelled mark_1(1), g_1(1)
- 7565921 to 7565921 labelled a__f_1(1), h_1(1), f_1(2)
- 7565921 to 7565922 labelled g_1(2)
- 7565923 to 7565921 labelled f_1(2)
- 7565922 to 7565923 labelled h_1(2)