(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(f(a)) → c(f(g(f(a))))
mark(f(X)) → a__f(mark(X))
mark(a) → a
mark(c(X)) → c(X)
mark(g(X)) → g(mark(X))
a__f(X) → f(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
1744381, 1744382, 1744383, 1744387, 1744385, 1744386, 1744384, 1744388, 1744389, 1744390, 1744392, 1744391, 1744396, 1744395, 1744393, 1744394
Node 1744381 is start node and node 1744382 is final node.
Those nodes are connect through the following edges:
- 1744381 to 1744382 labelled c_1(0), a(0), f_1(0)
- 1744381 to 1744383 labelled a__f_1(0), g_1(0), f_1(1)
- 1744381 to 1744384 labelled c_1(0)
- 1744381 to 1744389 labelled c_1(1)
- 1744382 to 1744382 labelled #_1(0)
- 1744383 to 1744382 labelled mark_1(0), c_1(1), a(1)
- 1744383 to 1744388 labelled a__f_1(1), g_1(1), f_1(2)
- 1744383 to 1744393 labelled c_1(2)
- 1744387 to 1744382 labelled a(0)
- 1744385 to 1744386 labelled g_1(0)
- 1744386 to 1744387 labelled f_1(0)
- 1744384 to 1744385 labelled f_1(0)
- 1744388 to 1744382 labelled mark_1(1), c_1(1), a(1)
- 1744388 to 1744388 labelled a__f_1(1), g_1(1), f_1(2)
- 1744388 to 1744393 labelled c_1(2)
- 1744389 to 1744390 labelled f_1(1)
- 1744390 to 1744391 labelled g_1(1)
- 1744392 to 1744382 labelled a(1)
- 1744391 to 1744392 labelled f_1(1)
- 1744396 to 1744382 labelled a(2)
- 1744395 to 1744396 labelled f_1(2)
- 1744393 to 1744394 labelled f_1(2)
- 1744394 to 1744395 labelled g_1(2)