(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:
8115738, 8115739, 8115740, 8115741, 8115742, 8115743, 8115744, 8115745, 8115746, 8115747, 8115748, 8115749, 8115750
Node 8115738 is start node and node 8115739 is final node.
Those nodes are connect through the following edges:
- 8115738 to 8115739 labelled g_1(0), a(0), f_1(0)
- 8115738 to 8115740 labelled a__f_1(0), f_1(1)
- 8115738 to 8115741 labelled a__f_1(0), f_1(1)
- 8115738 to 8115745 labelled a__f_1(1), f_1(2)
- 8115739 to 8115739 labelled #_1(0)
- 8115740 to 8115739 labelled mark_1(0), g_1(1), a(1)
- 8115740 to 8115744 labelled a__f_1(1), f_1(2)
- 8115740 to 8115748 labelled a__f_1(2), f_1(3)
- 8115741 to 8115742 labelled g_1(0)
- 8115742 to 8115743 labelled f_1(0)
- 8115743 to 8115739 labelled a(0)
- 8115744 to 8115739 labelled mark_1(1), g_1(1), a(1)
- 8115744 to 8115744 labelled a__f_1(1), f_1(2)
- 8115744 to 8115748 labelled a__f_1(2), f_1(3)
- 8115745 to 8115746 labelled g_1(1)
- 8115746 to 8115747 labelled f_1(1)
- 8115747 to 8115739 labelled a(1)
- 8115748 to 8115749 labelled g_1(2)
- 8115749 to 8115750 labelled f_1(2)
- 8115750 to 8115739 labelled a(2)