(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:
9977254, 9977255, 9977256, 9977259, 9977258, 9977257, 9977260, 9977261, 9977262, 9977263, 9977266, 9977264, 9977265
Node 9977254 is start node and node 9977255 is final node.
Those nodes are connect through the following edges:
- 9977254 to 9977255 labelled g_1(0), a(0), f_1(0)
- 9977254 to 9977256 labelled a__f_1(0), f_1(1)
- 9977254 to 9977257 labelled a__f_1(0), f_1(1)
- 9977254 to 9977261 labelled a__f_1(1), f_1(2)
- 9977255 to 9977255 labelled #_1(0)
- 9977256 to 9977255 labelled mark_1(0), g_1(1), a(1)
- 9977256 to 9977260 labelled a__f_1(1), f_1(2)
- 9977256 to 9977264 labelled a__f_1(2), f_1(3)
- 9977259 to 9977255 labelled a(0)
- 9977258 to 9977259 labelled f_1(0)
- 9977257 to 9977258 labelled g_1(0)
- 9977260 to 9977255 labelled mark_1(1), g_1(1), a(1)
- 9977260 to 9977260 labelled a__f_1(1), f_1(2)
- 9977260 to 9977264 labelled a__f_1(2), f_1(3)
- 9977261 to 9977262 labelled g_1(1)
- 9977262 to 9977263 labelled f_1(1)
- 9977263 to 9977255 labelled a(1)
- 9977266 to 9977255 labelled a(2)
- 9977264 to 9977265 labelled g_1(2)
- 9977265 to 9977266 labelled f_1(2)