(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(f(g(f(a))))
active(f(X)) → f(active(X))
f(mark(X)) → mark(f(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(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:
1750489, 1750490, 1750491, 1750494, 1750495, 1750493, 1750492, 1750496, 1750497, 1750498, 1750499, 1750500, 1750504, 1750502, 1750503, 1750501, 1750505, 1750506, 1750507, 1750508, 1750509, 1750510, 1750511, 1750512, 1750513, 1750515, 1750516, 1750514, 1750517, 1750518, 1750519, 1750520, 1750521, 1750522, 1750523, 1750524, 1750525, 1750526, 1750527, 1750528, 1750529, 1750530, 1750531, 1750532, 1750533, 1750534, 1750535, 1750536, 1750537, 1750538, 1750539, 1750540, 1750541
Node 1750489 is start node and node 1750490 is final node.
Those nodes are connect through the following edges:
- 1750489 to 1750491 labelled ok_1(0), mark_1(0)
- 1750489 to 1750492 labelled mark_1(0)
- 1750489 to 1750496 labelled top_1(0), g_1(0), f_1(0)
- 1750489 to 1750497 labelled f_1(0), top_1(0)
- 1750489 to 1750495 labelled ok_1(0)
- 1750489 to 1750506 labelled mark_1(1)
- 1750489 to 1750507 labelled top_1(1)
- 1750489 to 1750508 labelled ok_1(1)
- 1750489 to 1750519 labelled top_1(2)
- 1750489 to 1750536 labelled top_1(3)
- 1750490 to 1750490 labelled #_1(0)
- 1750491 to 1750490 labelled g_1(0), f_1(0)
- 1750491 to 1750500 labelled ok_1(1), mark_1(1)
- 1750494 to 1750495 labelled f_1(0)
- 1750495 to 1750490 labelled a(0)
- 1750493 to 1750494 labelled g_1(0)
- 1750492 to 1750493 labelled f_1(0)
- 1750496 to 1750490 labelled proper_1(0)
- 1750496 to 1750498 labelled g_1(1), f_1(1)
- 1750496 to 1750499 labelled ok_1(1)
- 1750496 to 1750511 labelled ok_1(2)
- 1750497 to 1750490 labelled active_1(0)
- 1750497 to 1750501 labelled mark_1(1)
- 1750497 to 1750505 labelled f_1(1)
- 1750497 to 1750509 labelled mark_1(2)
- 1750498 to 1750490 labelled proper_1(1)
- 1750498 to 1750498 labelled g_1(1), f_1(1)
- 1750498 to 1750499 labelled ok_1(1)
- 1750498 to 1750511 labelled ok_1(2)
- 1750499 to 1750490 labelled a(1)
- 1750500 to 1750490 labelled f_1(1), g_1(1)
- 1750500 to 1750500 labelled ok_1(1), mark_1(1)
- 1750504 to 1750490 labelled a(1)
- 1750502 to 1750503 labelled g_1(1)
- 1750503 to 1750504 labelled f_1(1)
- 1750501 to 1750502 labelled f_1(1)
- 1750505 to 1750490 labelled active_1(1)
- 1750505 to 1750501 labelled mark_1(1)
- 1750505 to 1750505 labelled f_1(1)
- 1750505 to 1750509 labelled mark_1(2)
- 1750506 to 1750501 labelled f_1(1)
- 1750506 to 1750509 labelled f_1(1)
- 1750507 to 1750501 labelled proper_1(1)
- 1750507 to 1750499 labelled active_1(1)
- 1750507 to 1750510 labelled f_1(2)
- 1750507 to 1750509 labelled proper_1(1)
- 1750507 to 1750511 labelled active_1(1)
- 1750507 to 1750514 labelled mark_1(2)
- 1750507 to 1750521 labelled mark_1(3)
- 1750507 to 1750527 labelled ok_1(3)
- 1750508 to 1750499 labelled g_1(1), f_1(1)
- 1750508 to 1750511 labelled g_1(1), f_1(1)
- 1750509 to 1750501 labelled f_1(2)
- 1750509 to 1750509 labelled f_1(2)
- 1750510 to 1750502 labelled proper_1(2)
- 1750510 to 1750512 labelled g_1(2)
- 1750510 to 1750511 labelled active_1(2)
- 1750510 to 1750509 labelled proper_1(2)
- 1750510 to 1750499 labelled active_1(2)
- 1750510 to 1750501 labelled proper_1(2)
- 1750510 to 1750518 labelled f_1(3)
- 1750510 to 1750510 labelled f_1(2)
- 1750510 to 1750514 labelled mark_1(2)
- 1750510 to 1750521 labelled mark_1(3)
- 1750510 to 1750523 labelled ok_1(3)
- 1750510 to 1750526 labelled mark_1(4)
- 1750510 to 1750527 labelled ok_1(3)
- 1750510 to 1750530 labelled ok_1(4)
- 1750511 to 1750499 labelled f_1(2), g_1(2)
- 1750511 to 1750511 labelled f_1(2), g_1(2)
- 1750512 to 1750503 labelled proper_1(2)
- 1750512 to 1750513 labelled f_1(2)
- 1750512 to 1750522 labelled ok_1(3)
- 1750513 to 1750504 labelled proper_1(2)
- 1750513 to 1750517 labelled ok_1(2)
- 1750515 to 1750516 labelled g_1(2)
- 1750516 to 1750517 labelled f_1(2)
- 1750514 to 1750515 labelled f_1(2)
- 1750517 to 1750490 labelled a(2)
- 1750518 to 1750511 labelled active_1(3)
- 1750518 to 1750509 labelled proper_1(3)
- 1750518 to 1750499 labelled active_1(3)
- 1750518 to 1750501 labelled proper_1(3)
- 1750518 to 1750518 labelled f_1(3)
- 1750518 to 1750510 labelled f_1(2)
- 1750518 to 1750514 labelled mark_1(2)
- 1750518 to 1750521 labelled mark_1(3)
- 1750518 to 1750526 labelled mark_1(4)
- 1750518 to 1750527 labelled ok_1(3)
- 1750518 to 1750530 labelled ok_1(4)
- 1750519 to 1750514 labelled proper_1(2)
- 1750519 to 1750520 labelled f_1(3)
- 1750519 to 1750521 labelled proper_1(2)
- 1750519 to 1750527 labelled active_1(2)
- 1750519 to 1750534 labelled ok_1(4)
- 1750520 to 1750515 labelled proper_1(3)
- 1750520 to 1750524 labelled g_1(3)
- 1750520 to 1750514 labelled proper_1(3)
- 1750520 to 1750521 labelled proper_1(3)
- 1750520 to 1750528 labelled f_1(4)
- 1750520 to 1750520 labelled f_1(3)
- 1750520 to 1750527 labelled active_1(3)
- 1750520 to 1750526 labelled proper_1(3)
- 1750520 to 1750523 labelled active_1(3)
- 1750520 to 1750530 labelled active_1(3)
- 1750520 to 1750533 labelled ok_1(4)
- 1750520 to 1750534 labelled ok_1(4)
- 1750520 to 1750535 labelled ok_1(5)
- 1750521 to 1750514 labelled f_1(3)
- 1750521 to 1750521 labelled f_1(3)
- 1750521 to 1750526 labelled f_1(3)
- 1750522 to 1750517 labelled f_1(3)
- 1750523 to 1750522 labelled g_1(3)
- 1750524 to 1750516 labelled proper_1(3)
- 1750524 to 1750525 labelled f_1(3)
- 1750524 to 1750531 labelled ok_1(4)
- 1750525 to 1750517 labelled proper_1(3)
- 1750525 to 1750529 labelled ok_1(3)
- 1750526 to 1750521 labelled f_1(4)
- 1750526 to 1750526 labelled f_1(4)
- 1750527 to 1750523 labelled f_1(3)
- 1750527 to 1750527 labelled f_1(3)
- 1750527 to 1750530 labelled f_1(3)
- 1750528 to 1750514 labelled proper_1(4)
- 1750528 to 1750521 labelled proper_1(4)
- 1750528 to 1750526 labelled proper_1(4)
- 1750528 to 1750528 labelled f_1(4)
- 1750528 to 1750520 labelled f_1(3)
- 1750528 to 1750530 labelled active_1(4)
- 1750528 to 1750532 labelled f_1(5)
- 1750528 to 1750527 labelled active_1(4)
- 1750528 to 1750523 labelled active_1(4)
- 1750528 to 1750534 labelled ok_1(4)
- 1750528 to 1750535 labelled ok_1(5)
- 1750528 to 1750538 labelled ok_1(6)
- 1750529 to 1750490 labelled a(3)
- 1750530 to 1750527 labelled f_1(4)
- 1750530 to 1750530 labelled f_1(4)
- 1750531 to 1750529 labelled f_1(4)
- 1750532 to 1750521 labelled proper_1(5)
- 1750532 to 1750526 labelled proper_1(5)
- 1750532 to 1750528 labelled f_1(4)
- 1750532 to 1750532 labelled f_1(5)
- 1750532 to 1750527 labelled active_1(5)
- 1750532 to 1750530 labelled active_1(5)
- 1750532 to 1750535 labelled ok_1(5)
- 1750532 to 1750538 labelled ok_1(6)
- 1750533 to 1750531 labelled g_1(4)
- 1750534 to 1750533 labelled f_1(4)
- 1750534 to 1750534 labelled f_1(4)
- 1750534 to 1750535 labelled f_1(4)
- 1750535 to 1750534 labelled f_1(5)
- 1750535 to 1750535 labelled f_1(5)
- 1750535 to 1750538 labelled f_1(5)
- 1750536 to 1750534 labelled active_1(3)
- 1750536 to 1750537 labelled f_1(4)
- 1750537 to 1750533 labelled active_1(4)
- 1750537 to 1750534 labelled active_1(4)
- 1750537 to 1750539 labelled f_1(5)
- 1750537 to 1750535 labelled active_1(4)
- 1750538 to 1750535 labelled f_1(6)
- 1750538 to 1750538 labelled f_1(6)
- 1750539 to 1750533 labelled active_1(5)
- 1750539 to 1750534 labelled active_1(5)
- 1750539 to 1750535 labelled active_1(5)
- 1750539 to 1750540 labelled f_1(6)
- 1750539 to 1750539 labelled f_1(5)
- 1750539 to 1750538 labelled active_1(5)
- 1750540 to 1750534 labelled active_1(6)
- 1750540 to 1750535 labelled active_1(6)
- 1750540 to 1750538 labelled active_1(6)
- 1750540 to 1750540 labelled f_1(6)
- 1750540 to 1750539 labelled f_1(5)
- 1750540 to 1750541 labelled f_1(7)
- 1750541 to 1750538 labelled active_1(7)
- 1750541 to 1750535 labelled active_1(7)
- 1750541 to 1750540 labelled f_1(6)
- 1750541 to 1750541 labelled f_1(7)