(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:
active(c) → mark(f(g(c)))
active(f(g(X))) → mark(g(X))
mark(c) → active(c)
mark(f(X)) → active(f(X))
mark(g(X)) → active(g(X))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
1914523, 1914524, 1914525, 1914527, 1914526, 1914530, 1914529, 1914528, 1914531, 1914532, 1914533, 1914534
Node 1914523 is start node and node 1914524 is final node.
Those nodes are connect through the following edges:
- 1914523 to 1914524 labelled g_1(0), f_1(0), g_1(1), f_1(1)
- 1914523 to 1914525 labelled mark_1(0)
- 1914523 to 1914523 labelled active_1(0), mark_1(0), active_1(1), mark_1(1)
- 1914523 to 1914527 labelled active_1(0), g_1(1)
- 1914523 to 1914528 labelled mark_1(1)
- 1914523 to 1914531 labelled active_1(1)
- 1914523 to 1914532 labelled active_1(2)
- 1914523 to 1914533 labelled mark_1(2)
- 1914523 to 1914534 labelled active_1(3)
- 1914524 to 1914524 labelled #_1(0)
- 1914525 to 1914526 labelled f_1(0)
- 1914527 to 1914524 labelled c(0)
- 1914526 to 1914527 labelled g_1(0)
- 1914530 to 1914524 labelled c(1)
- 1914529 to 1914530 labelled g_1(1)
- 1914528 to 1914529 labelled f_1(1)
- 1914531 to 1914524 labelled g_1(1)
- 1914531 to 1914526 labelled f_1(1)
- 1914532 to 1914524 labelled f_1(2), g_1(2), f_1(1), g_1(1)
- 1914532 to 1914529 labelled f_1(2)
- 1914532 to 1914527 labelled g_1(2)
- 1914533 to 1914530 labelled g_1(2)
- 1914534 to 1914530 labelled g_1(3)