(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:
a__f(f(a)) → a__f(g(f(a)))
mark(f(X)) → a__f(mark(X))
mark(a) → a
mark(g(X)) → g(X)
a__f(X) → f(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
1625763, 1625764, 1625765, 1625767, 1625768, 1625766, 1625769, 1625770, 1625771, 1625772, 1625773, 1625774, 1625775
Node 1625763 is start node and node 1625764 is final node.
Those nodes are connect through the following edges:
- 1625763 to 1625764 labelled g_1(0), a(0), f_1(0)
- 1625763 to 1625765 labelled a__f_1(0), f_1(1)
- 1625763 to 1625766 labelled a__f_1(0), f_1(1)
- 1625763 to 1625770 labelled a__f_1(1), f_1(2)
- 1625764 to 1625764 labelled #_1(0)
- 1625765 to 1625764 labelled mark_1(0), g_1(1), a(1)
- 1625765 to 1625769 labelled a__f_1(1), f_1(2)
- 1625765 to 1625773 labelled a__f_1(2), f_1(3)
- 1625767 to 1625768 labelled f_1(0)
- 1625768 to 1625764 labelled a(0)
- 1625766 to 1625767 labelled g_1(0)
- 1625769 to 1625764 labelled mark_1(1), g_1(1), a(1)
- 1625769 to 1625769 labelled a__f_1(1), f_1(2)
- 1625769 to 1625773 labelled a__f_1(2), f_1(3)
- 1625770 to 1625771 labelled g_1(1)
- 1625771 to 1625772 labelled f_1(1)
- 1625772 to 1625764 labelled a(1)
- 1625773 to 1625774 labelled g_1(2)
- 1625774 to 1625775 labelled f_1(2)
- 1625775 to 1625764 labelled a(2)