(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 7. This implies Q-termination of R.
The following rules were used to construct the certificate:
active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(X)) → f(active(X))
active(g(X)) → g(active(X))
f(mark(X)) → mark(f(X))
g(mark(X)) → mark(g(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(c(X)) → c(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
c(ok(X)) → ok(c(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
8248323, 8248324, 8248325, 8248330, 8248327, 8248328, 8248326, 8248329, 8248331, 8248332, 8248333, 8248334, 8248337, 8248338, 8248335, 8248336, 8248339, 8248340, 8248341, 8248342, 8248343, 8248344, 8248345, 8248346, 8248347, 8248348, 8248349, 8248353, 8248354, 8248352, 8248350, 8248351, 8248355, 8248356, 8248357, 8248358, 8248359, 8248360, 8248361, 8248362, 8248363, 8248364, 8248365, 8248366, 8248367, 8248368, 8248369, 8248370, 8248371, 8248372, 8248373, 8248374, 8248375, 8248376, 8248377, 8248378, 8248379, 8248380, 8248381, 8248382, 8248383, 8248384, 8248385, 8248386
Node 8248323 is start node and node 8248324 is final node.
Those nodes are connect through the following edges:
- 8248323 to 8248325 labelled ok_1(0), mark_1(0)
- 8248323 to 8248326 labelled mark_1(0), ok_1(0)
- 8248323 to 8248331 labelled g_1(0), top_1(0), f_1(0), c_1(0)
- 8248323 to 8248330 labelled ok_1(0)
- 8248323 to 8248341 labelled ok_1(1)
- 8248323 to 8248342 labelled top_1(1)
- 8248323 to 8248343 labelled mark_1(1)
- 8248323 to 8248356 labelled top_1(2)
- 8248323 to 8248379 labelled top_1(3)
- 8248324 to 8248324 labelled #_1(0)
- 8248325 to 8248324 labelled g_1(0), c_1(0)
- 8248325 to 8248332 labelled ok_1(1), mark_1(1)
- 8248330 to 8248324 labelled a(0)
- 8248327 to 8248328 labelled f_1(0)
- 8248328 to 8248329 labelled g_1(0)
- 8248326 to 8248327 labelled c_1(0)
- 8248326 to 8248324 labelled f_1(0)
- 8248326 to 8248340 labelled mark_1(1), ok_1(1)
- 8248329 to 8248330 labelled f_1(0)
- 8248331 to 8248324 labelled proper_1(0), active_1(0)
- 8248331 to 8248333 labelled g_1(1), f_1(1), c_1(1)
- 8248331 to 8248334 labelled ok_1(1)
- 8248331 to 8248335 labelled mark_1(1)
- 8248331 to 8248345 labelled ok_1(2)
- 8248331 to 8248346 labelled mark_1(2)
- 8248332 to 8248324 labelled g_1(1), c_1(1)
- 8248332 to 8248332 labelled ok_1(1), mark_1(1)
- 8248333 to 8248324 labelled proper_1(1), active_1(1)
- 8248333 to 8248335 labelled mark_1(1)
- 8248333 to 8248333 labelled g_1(1), f_1(1), c_1(1)
- 8248333 to 8248334 labelled ok_1(1)
- 8248333 to 8248345 labelled ok_1(2)
- 8248333 to 8248346 labelled mark_1(2)
- 8248334 to 8248324 labelled a(1)
- 8248337 to 8248338 labelled g_1(1)
- 8248338 to 8248339 labelled f_1(1)
- 8248335 to 8248336 labelled c_1(1)
- 8248336 to 8248337 labelled f_1(1)
- 8248339 to 8248324 labelled a(1)
- 8248340 to 8248324 labelled f_1(1)
- 8248340 to 8248340 labelled mark_1(1), ok_1(1)
- 8248341 to 8248334 labelled c_1(1), f_1(1), g_1(1)
- 8248341 to 8248345 labelled c_1(1), f_1(1), g_1(1)
- 8248342 to 8248334 labelled active_1(1)
- 8248342 to 8248335 labelled proper_1(1)
- 8248342 to 8248344 labelled c_1(2)
- 8248342 to 8248346 labelled proper_1(1)
- 8248342 to 8248345 labelled active_1(1)
- 8248342 to 8248348 labelled f_1(2), g_1(2)
- 8248342 to 8248350 labelled mark_1(2)
- 8248342 to 8248358 labelled mark_1(3)
- 8248342 to 8248371 labelled ok_1(3)
- 8248343 to 8248335 labelled f_1(1), g_1(1)
- 8248343 to 8248346 labelled f_1(1), g_1(1)
- 8248344 to 8248336 labelled proper_1(2)
- 8248344 to 8248347 labelled f_1(2)
- 8248344 to 8248367 labelled ok_1(3)
- 8248345 to 8248334 labelled g_1(2), c_1(2), f_1(2)
- 8248345 to 8248345 labelled g_1(2), c_1(2), f_1(2)
- 8248346 to 8248335 labelled g_1(2), f_1(2)
- 8248346 to 8248346 labelled g_1(2), f_1(2)
- 8248347 to 8248337 labelled proper_1(2)
- 8248347 to 8248349 labelled g_1(2)
- 8248347 to 8248364 labelled ok_1(3)
- 8248348 to 8248346 labelled proper_1(2)
- 8248348 to 8248334 labelled active_1(2)
- 8248348 to 8248345 labelled active_1(2)
- 8248348 to 8248335 labelled proper_1(2)
- 8248348 to 8248344 labelled c_1(2)
- 8248348 to 8248355 labelled f_1(3), g_1(3)
- 8248348 to 8248350 labelled mark_1(2)
- 8248348 to 8248358 labelled mark_1(3)
- 8248348 to 8248362 labelled mark_1(4)
- 8248348 to 8248371 labelled ok_1(3)
- 8248348 to 8248374 labelled ok_1(4)
- 8248349 to 8248338 labelled proper_1(2)
- 8248349 to 8248357 labelled f_1(2)
- 8248349 to 8248361 labelled ok_1(3)
- 8248353 to 8248354 labelled f_1(2)
- 8248354 to 8248324 labelled a(2)
- 8248352 to 8248353 labelled g_1(2)
- 8248350 to 8248351 labelled c_1(2)
- 8248351 to 8248352 labelled f_1(2)
- 8248355 to 8248346 labelled proper_1(3)
- 8248355 to 8248334 labelled active_1(3)
- 8248355 to 8248345 labelled active_1(3)
- 8248355 to 8248335 labelled proper_1(3)
- 8248355 to 8248344 labelled c_1(2)
- 8248355 to 8248355 labelled f_1(3), g_1(3)
- 8248355 to 8248350 labelled mark_1(2)
- 8248355 to 8248358 labelled mark_1(3)
- 8248355 to 8248362 labelled mark_1(4)
- 8248355 to 8248371 labelled ok_1(3)
- 8248355 to 8248374 labelled ok_1(4)
- 8248356 to 8248350 labelled proper_1(2)
- 8248356 to 8248359 labelled c_1(3)
- 8248356 to 8248358 labelled proper_1(2)
- 8248356 to 8248363 labelled g_1(3), f_1(3)
- 8248356 to 8248371 labelled active_1(2)
- 8248356 to 8248377 labelled ok_1(4)
- 8248357 to 8248339 labelled proper_1(2)
- 8248357 to 8248354 labelled ok_1(2)
- 8248358 to 8248350 labelled g_1(3), f_1(3)
- 8248358 to 8248358 labelled g_1(3), f_1(3)
- 8248358 to 8248362 labelled g_1(3), f_1(3)
- 8248359 to 8248351 labelled proper_1(3)
- 8248359 to 8248360 labelled f_1(3)
- 8248359 to 8248376 labelled ok_1(4)
- 8248360 to 8248352 labelled proper_1(3)
- 8248360 to 8248365 labelled g_1(3)
- 8248360 to 8248375 labelled ok_1(4)
- 8248361 to 8248354 labelled f_1(3)
- 8248362 to 8248358 labelled f_1(4), g_1(4)
- 8248362 to 8248362 labelled f_1(4), g_1(4)
- 8248363 to 8248350 labelled proper_1(3)
- 8248363 to 8248358 labelled proper_1(3)
- 8248363 to 8248359 labelled c_1(3)
- 8248363 to 8248362 labelled proper_1(3)
- 8248363 to 8248368 labelled f_1(4), g_1(4)
- 8248363 to 8248369 labelled g_1(4), f_1(4)
- 8248363 to 8248371 labelled active_1(3)
- 8248363 to 8248374 labelled active_1(3)
- 8248363 to 8248377 labelled ok_1(4)
- 8248363 to 8248378 labelled ok_1(5)
- 8248364 to 8248361 labelled g_1(3)
- 8248365 to 8248353 labelled proper_1(3)
- 8248365 to 8248366 labelled f_1(3)
- 8248365 to 8248373 labelled ok_1(4)
- 8248366 to 8248354 labelled proper_1(3)
- 8248366 to 8248370 labelled ok_1(3)
- 8248367 to 8248364 labelled f_1(3)
- 8248368 to 8248362 labelled proper_1(4)
- 8248368 to 8248350 labelled proper_1(4)
- 8248368 to 8248359 labelled c_1(3)
- 8248368 to 8248372 labelled g_1(5), f_1(5)
- 8248368 to 8248374 labelled active_1(4)
- 8248368 to 8248371 labelled active_1(4)
- 8248368 to 8248368 labelled g_1(4), f_1(4)
- 8248368 to 8248377 labelled ok_1(4)
- 8248368 to 8248378 labelled ok_1(5)
- 8248368 to 8248381 labelled ok_1(6)
- 8248368 to 8248380 labelled ok_1(6)
- 8248369 to 8248358 labelled proper_1(4)
- 8248369 to 8248368 labelled f_1(4), g_1(4)
- 8248369 to 8248369 labelled g_1(4), f_1(4)
- 8248369 to 8248378 labelled ok_1(5)
- 8248370 to 8248324 labelled a(3)
- 8248371 to 8248367 labelled c_1(3)
- 8248371 to 8248371 labelled g_1(3), f_1(3)
- 8248371 to 8248374 labelled g_1(3), f_1(3)
- 8248372 to 8248358 labelled proper_1(5)
- 8248372 to 8248362 labelled proper_1(5)
- 8248372 to 8248368 labelled f_1(4), g_1(4)
- 8248372 to 8248369 labelled g_1(4), f_1(4)
- 8248372 to 8248372 labelled g_1(5), f_1(5)
- 8248372 to 8248374 labelled active_1(5)
- 8248372 to 8248371 labelled active_1(5)
- 8248372 to 8248378 labelled ok_1(5)
- 8248372 to 8248380 labelled ok_1(6)
- 8248372 to 8248381 labelled ok_1(6)
- 8248373 to 8248370 labelled f_1(4)
- 8248374 to 8248371 labelled f_1(4), g_1(4)
- 8248374 to 8248374 labelled f_1(4), g_1(4)
- 8248375 to 8248373 labelled g_1(4)
- 8248376 to 8248375 labelled f_1(4)
- 8248377 to 8248376 labelled c_1(4)
- 8248377 to 8248377 labelled f_1(4), g_1(4)
- 8248377 to 8248378 labelled f_1(4), g_1(4)
- 8248378 to 8248377 labelled g_1(5), f_1(5)
- 8248378 to 8248378 labelled f_1(5), g_1(5)
- 8248378 to 8248381 labelled g_1(5), f_1(5)
- 8248378 to 8248380 labelled g_1(5), f_1(5)
- 8248379 to 8248377 labelled active_1(3)
- 8248379 to 8248382 labelled g_1(4), f_1(4)
- 8248380 to 8248378 labelled f_1(6)
- 8248380 to 8248381 labelled f_1(6)
- 8248380 to 8248380 labelled f_1(6)
- 8248381 to 8248378 labelled g_1(6)
- 8248381 to 8248381 labelled g_1(6)
- 8248381 to 8248380 labelled g_1(6)
- 8248382 to 8248377 labelled active_1(4)
- 8248382 to 8248378 labelled active_1(4)
- 8248382 to 8248383 labelled f_1(5), g_1(5)
- 8248383 to 8248378 labelled active_1(5)
- 8248383 to 8248377 labelled active_1(5)
- 8248383 to 8248383 labelled f_1(5), g_1(5)
- 8248383 to 8248384 labelled f_1(6), g_1(6)
- 8248383 to 8248385 labelled g_1(6), f_1(6)
- 8248383 to 8248380 labelled active_1(5)
- 8248383 to 8248381 labelled active_1(5)
- 8248384 to 8248377 labelled active_1(6)
- 8248384 to 8248380 labelled active_1(6)
- 8248384 to 8248381 labelled active_1(6)
- 8248384 to 8248383 labelled f_1(5), g_1(5)
- 8248384 to 8248386 labelled f_1(7), g_1(7)
- 8248385 to 8248378 labelled active_1(6)
- 8248385 to 8248384 labelled f_1(6), g_1(6)
- 8248385 to 8248385 labelled g_1(6), f_1(6)
- 8248386 to 8248380 labelled active_1(7)
- 8248386 to 8248381 labelled active_1(7)
- 8248386 to 8248378 labelled active_1(7)
- 8248386 to 8248384 labelled f_1(6), g_1(6)
- 8248386 to 8248385 labelled g_1(6), f_1(6)
- 8248386 to 8248386 labelled f_1(7), g_1(7)