(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(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(X))
mark(a) → active(a)
mark(g(X)) → active(g(mark(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:
10064369, 10064370, 10064372, 10064373, 10064374, 10064371, 10064375, 10064376, 10064378, 10064377, 10064379, 10064380, 10064381, 10064383, 10064382, 10064384
Node 10064369 is start node and node 10064370 is final node.
Those nodes are connect through the following edges:
- 10064369 to 10064370 labelled g_1(0), f_1(0), f_1(1), g_1(1)
- 10064369 to 10064371 labelled mark_1(0)
- 10064369 to 10064375 labelled active_1(0)
- 10064369 to 10064369 labelled active_1(0)
- 10064369 to 10064374 labelled active_1(0)
- 10064369 to 10064379 labelled active_1(1)
- 10064369 to 10064380 labelled mark_1(1)
- 10064369 to 10064384 labelled active_1(2)
- 10064370 to 10064370 labelled #_1(0)
- 10064372 to 10064373 labelled g_1(0)
- 10064373 to 10064374 labelled f_1(0)
- 10064374 to 10064370 labelled a(0)
- 10064371 to 10064372 labelled f_1(0)
- 10064375 to 10064376 labelled g_1(0)
- 10064375 to 10064370 labelled g_1(1)
- 10064375 to 10064369 labelled g_1(1)
- 10064375 to 10064377 labelled g_1(1)
- 10064375 to 10064380 labelled g_1(2), g_1(1)
- 10064375 to 10064379 labelled g_1(2)
- 10064375 to 10064384 labelled g_1(2), g_1(1)
- 10064375 to 10064371 labelled g_1(1)
- 10064375 to 10064374 labelled g_1(1)
- 10064375 to 10064375 labelled g_1(1)
- 10064376 to 10064370 labelled mark_1(0)
- 10064376 to 10064377 labelled active_1(1)
- 10064376 to 10064369 labelled active_1(1)
- 10064376 to 10064380 labelled mark_1(1)
- 10064376 to 10064384 labelled active_1(2)
- 10064378 to 10064370 labelled mark_1(1)
- 10064378 to 10064377 labelled active_1(1)
- 10064378 to 10064369 labelled active_1(1)
- 10064378 to 10064380 labelled mark_1(1)
- 10064378 to 10064384 labelled active_1(2)
- 10064377 to 10064378 labelled g_1(1)
- 10064377 to 10064370 labelled a(1), g_1(2), g_1(1)
- 10064377 to 10064369 labelled g_1(2), g_1(1)
- 10064377 to 10064377 labelled g_1(2)
- 10064377 to 10064379 labelled g_1(2)
- 10064377 to 10064380 labelled g_1(2)
- 10064377 to 10064384 labelled g_1(3), g_1(2)
- 10064377 to 10064371 labelled g_1(1)
- 10064377 to 10064374 labelled g_1(1)
- 10064377 to 10064375 labelled g_1(1)
- 10064379 to 10064372 labelled f_1(1)
- 10064380 to 10064381 labelled f_1(1)
- 10064381 to 10064382 labelled g_1(1)
- 10064383 to 10064370 labelled a(1)
- 10064382 to 10064383 labelled f_1(1)
- 10064384 to 10064381 labelled f_1(2)