(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:
10131568, 10131569, 10131570, 10131572, 10131573, 10131571, 10131574, 10131575, 10131576, 10131577, 10131578, 10131579, 10131583, 10131580, 10131581, 10131582, 10131584, 10131585, 10131586, 10131587, 10131588, 10131589, 10131590, 10131591, 10131592, 10131595, 10131596, 10131593, 10131594, 10131597, 10131598, 10131599, 10131600, 10131601, 10131602, 10131603, 10131604, 10131605, 10131606, 10131607, 10131608, 10131609, 10131610, 10131611, 10131612, 10131613, 10131614, 10131615, 10131616, 10131617, 10131618, 10131619, 10131620, 10131621, 10131622, 10131623, 10131624
Node 10131568 is start node and node 10131569 is final node.
Those nodes are connect through the following edges:
- 10131568 to 10131570 labelled ok_1(0), mark_1(0)
- 10131568 to 10131571 labelled mark_1(0)
- 10131568 to 10131575 labelled top_1(0), g_1(0), f_1(0)
- 10131568 to 10131576 labelled f_1(0), top_1(0)
- 10131568 to 10131574 labelled ok_1(0)
- 10131568 to 10131585 labelled top_1(1)
- 10131568 to 10131586 labelled mark_1(1)
- 10131568 to 10131587 labelled ok_1(1)
- 10131568 to 10131597 labelled top_1(2)
- 10131568 to 10131616 labelled top_1(3)
- 10131569 to 10131569 labelled #_1(0)
- 10131570 to 10131569 labelled g_1(0), f_1(0)
- 10131570 to 10131579 labelled ok_1(1), mark_1(1)
- 10131572 to 10131573 labelled g_1(0)
- 10131573 to 10131574 labelled f_1(0)
- 10131571 to 10131572 labelled f_1(0)
- 10131574 to 10131569 labelled a(0)
- 10131575 to 10131569 labelled proper_1(0)
- 10131575 to 10131577 labelled g_1(1), f_1(1)
- 10131575 to 10131578 labelled ok_1(1)
- 10131575 to 10131588 labelled ok_1(2)
- 10131576 to 10131569 labelled active_1(0)
- 10131576 to 10131580 labelled mark_1(1)
- 10131576 to 10131584 labelled f_1(1)
- 10131576 to 10131590 labelled mark_1(2)
- 10131577 to 10131569 labelled proper_1(1)
- 10131577 to 10131577 labelled g_1(1), f_1(1)
- 10131577 to 10131578 labelled ok_1(1)
- 10131577 to 10131588 labelled ok_1(2)
- 10131578 to 10131569 labelled a(1)
- 10131579 to 10131569 labelled g_1(1), f_1(1)
- 10131579 to 10131579 labelled ok_1(1), mark_1(1)
- 10131583 to 10131569 labelled a(1)
- 10131580 to 10131581 labelled f_1(1)
- 10131581 to 10131582 labelled g_1(1)
- 10131582 to 10131583 labelled f_1(1)
- 10131584 to 10131569 labelled active_1(1)
- 10131584 to 10131580 labelled mark_1(1)
- 10131584 to 10131584 labelled f_1(1)
- 10131584 to 10131590 labelled mark_1(2)
- 10131585 to 10131580 labelled proper_1(1)
- 10131585 to 10131578 labelled active_1(1)
- 10131585 to 10131589 labelled f_1(2)
- 10131585 to 10131588 labelled active_1(1)
- 10131585 to 10131590 labelled proper_1(1)
- 10131585 to 10131593 labelled mark_1(2)
- 10131585 to 10131600 labelled mark_1(3)
- 10131585 to 10131603 labelled ok_1(3)
- 10131586 to 10131580 labelled f_1(1)
- 10131586 to 10131590 labelled f_1(1)
- 10131587 to 10131578 labelled f_1(1), g_1(1)
- 10131587 to 10131588 labelled f_1(1), g_1(1)
- 10131588 to 10131578 labelled f_1(2), g_1(2)
- 10131588 to 10131588 labelled f_1(2), g_1(2)
- 10131589 to 10131581 labelled proper_1(2)
- 10131589 to 10131591 labelled g_1(2)
- 10131589 to 10131590 labelled proper_1(2)
- 10131589 to 10131578 labelled active_1(2)
- 10131589 to 10131588 labelled active_1(2)
- 10131589 to 10131580 labelled proper_1(2)
- 10131589 to 10131598 labelled f_1(3)
- 10131589 to 10131589 labelled f_1(2)
- 10131589 to 10131593 labelled mark_1(2)
- 10131589 to 10131600 labelled mark_1(3)
- 10131589 to 10131603 labelled ok_1(3)
- 10131589 to 10131605 labelled mark_1(4)
- 10131589 to 10131606 labelled ok_1(4)
- 10131590 to 10131580 labelled f_1(2)
- 10131590 to 10131590 labelled f_1(2)
- 10131591 to 10131582 labelled proper_1(2)
- 10131591 to 10131592 labelled f_1(2)
- 10131591 to 10131599 labelled ok_1(3)
- 10131592 to 10131583 labelled proper_1(2)
- 10131592 to 10131596 labelled ok_1(2)
- 10131595 to 10131596 labelled f_1(2)
- 10131596 to 10131569 labelled a(2)
- 10131593 to 10131594 labelled f_1(2)
- 10131594 to 10131595 labelled g_1(2)
- 10131597 to 10131593 labelled proper_1(2)
- 10131597 to 10131601 labelled f_1(3)
- 10131597 to 10131600 labelled proper_1(2)
- 10131597 to 10131603 labelled active_1(2)
- 10131597 to 10131614 labelled ok_1(4)
- 10131598 to 10131590 labelled proper_1(3)
- 10131598 to 10131578 labelled active_1(3)
- 10131598 to 10131588 labelled active_1(3)
- 10131598 to 10131580 labelled proper_1(3)
- 10131598 to 10131598 labelled f_1(3)
- 10131598 to 10131589 labelled f_1(2)
- 10131598 to 10131593 labelled mark_1(2)
- 10131598 to 10131600 labelled mark_1(3)
- 10131598 to 10131603 labelled ok_1(3)
- 10131598 to 10131605 labelled mark_1(4)
- 10131598 to 10131606 labelled ok_1(4)
- 10131599 to 10131596 labelled f_1(3)
- 10131600 to 10131593 labelled f_1(3)
- 10131600 to 10131600 labelled f_1(3)
- 10131600 to 10131605 labelled f_1(3)
- 10131601 to 10131594 labelled proper_1(3)
- 10131601 to 10131602 labelled g_1(3)
- 10131601 to 10131593 labelled proper_1(3)
- 10131601 to 10131600 labelled proper_1(3)
- 10131601 to 10131601 labelled f_1(3)
- 10131601 to 10131607 labelled f_1(4)
- 10131601 to 10131605 labelled proper_1(3)
- 10131601 to 10131609 labelled f_1(4)
- 10131601 to 10131603 labelled active_1(3)
- 10131601 to 10131606 labelled active_1(3)
- 10131601 to 10131611 labelled ok_1(4)
- 10131601 to 10131614 labelled ok_1(4)
- 10131601 to 10131615 labelled ok_1(5)
- 10131601 to 10131618 labelled ok_1(5)
- 10131602 to 10131595 labelled proper_1(3)
- 10131602 to 10131604 labelled f_1(3)
- 10131602 to 10131610 labelled ok_1(4)
- 10131603 to 10131599 labelled g_1(3)
- 10131603 to 10131603 labelled f_1(3)
- 10131603 to 10131606 labelled f_1(3)
- 10131604 to 10131596 labelled proper_1(3)
- 10131604 to 10131608 labelled ok_1(3)
- 10131605 to 10131600 labelled f_1(4)
- 10131605 to 10131605 labelled f_1(4)
- 10131606 to 10131603 labelled f_1(4)
- 10131606 to 10131606 labelled f_1(4)
- 10131607 to 10131593 labelled proper_1(4)
- 10131607 to 10131600 labelled proper_1(4)
- 10131607 to 10131601 labelled f_1(3)
- 10131607 to 10131609 labelled f_1(4)
- 10131607 to 10131607 labelled f_1(4)
- 10131607 to 10131603 labelled active_1(4)
- 10131607 to 10131606 labelled active_1(4)
- 10131607 to 10131613 labelled f_1(5)
- 10131607 to 10131614 labelled ok_1(4)
- 10131607 to 10131615 labelled ok_1(5)
- 10131607 to 10131618 labelled ok_1(5)
- 10131607 to 10131620 labelled ok_1(6)
- 10131607 to 10131617 labelled ok_1(6)
- 10131608 to 10131569 labelled a(3)
- 10131609 to 10131605 labelled proper_1(4)
- 10131609 to 10131612 labelled f_1(5)
- 10131609 to 10131617 labelled ok_1(6)
- 10131609 to 10131620 labelled ok_1(6)
- 10131610 to 10131608 labelled f_1(4)
- 10131611 to 10131610 labelled g_1(4)
- 10131612 to 10131605 labelled proper_1(5)
- 10131612 to 10131600 labelled proper_1(5)
- 10131612 to 10131609 labelled f_1(4)
- 10131612 to 10131607 labelled f_1(4)
- 10131612 to 10131612 labelled f_1(5)
- 10131612 to 10131615 labelled ok_1(5)
- 10131612 to 10131617 labelled ok_1(6)
- 10131612 to 10131618 labelled ok_1(5)
- 10131612 to 10131620 labelled ok_1(6)
- 10131613 to 10131603 labelled active_1(5)
- 10131613 to 10131606 labelled active_1(5)
- 10131613 to 10131613 labelled f_1(5)
- 10131613 to 10131607 labelled f_1(4)
- 10131613 to 10131618 labelled ok_1(5)
- 10131613 to 10131615 labelled ok_1(5)
- 10131613 to 10131620 labelled ok_1(6)
- 10131613 to 10131617 labelled ok_1(6)
- 10131614 to 10131611 labelled f_1(4)
- 10131614 to 10131614 labelled f_1(4)
- 10131614 to 10131615 labelled f_1(4)
- 10131614 to 10131618 labelled f_1(4)
- 10131615 to 10131614 labelled f_1(5)
- 10131615 to 10131617 labelled f_1(5)
- 10131616 to 10131614 labelled active_1(3)
- 10131616 to 10131619 labelled f_1(4)
- 10131617 to 10131615 labelled f_1(6)
- 10131617 to 10131617 labelled f_1(6)
- 10131617 to 10131620 labelled f_1(6)
- 10131618 to 10131615 labelled f_1(5)
- 10131618 to 10131618 labelled f_1(5)
- 10131618 to 10131620 labelled f_1(5)
- 10131619 to 10131611 labelled active_1(4)
- 10131619 to 10131614 labelled active_1(4)
- 10131619 to 10131621 labelled f_1(5)
- 10131619 to 10131615 labelled active_1(4)
- 10131619 to 10131618 labelled active_1(4)
- 10131620 to 10131618 labelled f_1(6)
- 10131621 to 10131611 labelled active_1(5)
- 10131621 to 10131615 labelled active_1(5)
- 10131621 to 10131614 labelled active_1(5)
- 10131621 to 10131621 labelled f_1(5)
- 10131621 to 10131617 labelled active_1(5)
- 10131621 to 10131622 labelled f_1(6)
- 10131621 to 10131618 labelled active_1(5)
- 10131621 to 10131620 labelled active_1(5)
- 10131622 to 10131617 labelled active_1(6)
- 10131622 to 10131614 labelled active_1(6)
- 10131622 to 10131620 labelled active_1(6)
- 10131622 to 10131623 labelled f_1(7)
- 10131622 to 10131618 labelled active_1(6)
- 10131622 to 10131621 labelled f_1(5)
- 10131622 to 10131615 labelled active_1(6)
- 10131622 to 10131624 labelled f_1(7)
- 10131622 to 10131622 labelled f_1(6)
- 10131623 to 10131620 labelled active_1(7)
- 10131623 to 10131617 labelled active_1(7)
- 10131623 to 10131615 labelled active_1(7)
- 10131623 to 10131624 labelled f_1(7)
- 10131623 to 10131623 labelled f_1(7)
- 10131623 to 10131622 labelled f_1(6)
- 10131624 to 10131618 labelled active_1(7)
- 10131624 to 10131622 labelled f_1(6)