(3) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 6. This implies Q-termination of R.
The following rules were used to construct the certificate:
c'(active(x)) → c'(g(f(mark(x))))
g(f(active(x))) → g(mark(x))
c'(proper(x)) → c'(ok(x))
f(proper(x)) → proper(f(x))
g(proper(x)) → proper(g(x))
ok(f(x)) → f(ok(x))
ok(g(x)) → g(ok(x))
mark(top(x)) → proper(top(x))
ok(top(x)) → active(top(x))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
8005616, 8005617, 8005618, 8005619, 8005620, 8005621, 8005622, 8005623, 8005624, 8005625, 8005626, 8005627, 8005628, 8005629, 8005630, 8005631, 8005632, 8005633, 8005634, 8005635, 8005636, 8005637, 8005639, 8005638, 8005640, 8005641, 8005642, 8005643, 8005644, 8005645, 8005646, 8005647, 8005648, 8005649, 8005650, 8005651, 8005652, 8005653, 8005654, 8005655, 8005656, 8005657, 8005658, 8005659, 8005660, 8005661, 8005662, 8005663, 8005664, 8005665, 8005666, 8005667, 8005668, 8005669, 8005670, 8005671, 8005672, 8005673, 8005674, 8005675, 8005676
Node 8005616 is start node and node 8005617 is final node.
Those nodes are connect through the following edges:
- 8005616 to 8005618 labelled proper_1(0)
- 8005616 to 8005619 labelled active_1(0), proper_1(0)
- 8005616 to 8005620 labelled g_1(0), f_1(0), c'_1(0)
- 8005616 to 8005621 labelled c'_1(0)
- 8005616 to 8005628 labelled c'_1(1)
- 8005616 to 8005629 labelled proper_1(1)
- 8005616 to 8005630 labelled c'_1(1)
- 8005616 to 8005632 labelled g_1(1)
- 8005616 to 8005637 labelled c'_1(2)
- 8005616 to 8005641 labelled proper_1(2)
- 8005616 to 8005652 labelled c'_1(3)
- 8005616 to 8005668 labelled c'_1(4)
- 8005617 to 8005617 labelled #_1(0)
- 8005618 to 8005617 labelled g_1(0), f_1(0)
- 8005618 to 8005624 labelled proper_1(1)
- 8005618 to 8005627 labelled g_1(1)
- 8005618 to 8005635 labelled proper_1(2)
- 8005619 to 8005617 labelled top_1(0)
- 8005620 to 8005617 labelled ok_1(0), mark_1(0)
- 8005620 to 8005625 labelled proper_1(1), active_1(1)
- 8005620 to 8005626 labelled g_1(1), f_1(1)
- 8005620 to 8005636 labelled g_1(2)
- 8005620 to 8005643 labelled proper_1(3)
- 8005620 to 8005648 labelled proper_1(2)
- 8005621 to 8005622 labelled g_1(0)
- 8005621 to 8005634 labelled proper_1(1)
- 8005622 to 8005623 labelled f_1(0)
- 8005622 to 8005629 labelled proper_1(1)
- 8005623 to 8005617 labelled mark_1(0)
- 8005623 to 8005625 labelled proper_1(1)
- 8005624 to 8005617 labelled f_1(1), g_1(1)
- 8005624 to 8005624 labelled proper_1(1)
- 8005624 to 8005627 labelled g_1(1)
- 8005624 to 8005635 labelled proper_1(2)
- 8005625 to 8005617 labelled top_1(1)
- 8005626 to 8005617 labelled ok_1(1)
- 8005626 to 8005625 labelled active_1(1)
- 8005626 to 8005626 labelled g_1(1), f_1(1)
- 8005626 to 8005636 labelled g_1(2)
- 8005626 to 8005643 labelled proper_1(3)
- 8005626 to 8005648 labelled proper_1(2)
- 8005627 to 8005617 labelled mark_1(1)
- 8005627 to 8005625 labelled proper_1(1)
- 8005628 to 8005625 labelled ok_1(1)
- 8005628 to 8005633 labelled active_1(2)
- 8005628 to 8005634 labelled ok_1(1)
- 8005628 to 8005644 labelled g_1(2)
- 8005628 to 8005643 labelled ok_1(1)
- 8005628 to 8005648 labelled ok_1(1)
- 8005628 to 8005647 labelled g_1(2), f_1(2)
- 8005628 to 8005653 labelled g_1(3)
- 8005628 to 8005656 labelled proper_1(4)
- 8005628 to 8005660 labelled g_1(3)
- 8005628 to 8005664 labelled proper_1(3)
- 8005629 to 8005625 labelled g_1(1), f_1(1)
- 8005629 to 8005643 labelled f_1(1), g_1(1)
- 8005629 to 8005648 labelled f_1(1), g_1(1)
- 8005630 to 8005631 labelled g_1(1)
- 8005630 to 8005642 labelled proper_1(2)
- 8005631 to 8005632 labelled f_1(1)
- 8005631 to 8005640 labelled proper_1(2)
- 8005632 to 8005625 labelled mark_1(1)
- 8005632 to 8005633 labelled proper_1(2)
- 8005633 to 8005617 labelled top_1(2)
- 8005634 to 8005629 labelled g_1(1)
- 8005635 to 8005625 labelled g_1(2)
- 8005636 to 8005625 labelled mark_1(2)
- 8005636 to 8005633 labelled proper_1(2)
- 8005637 to 8005638 labelled g_1(2)
- 8005637 to 8005642 labelled ok_1(2)
- 8005637 to 8005649 labelled g_1(3)
- 8005637 to 8005650 labelled proper_1(3)
- 8005637 to 8005659 labelled g_1(4)
- 8005637 to 8005656 labelled ok_1(2)
- 8005637 to 8005662 labelled proper_1(5)
- 8005637 to 8005664 labelled ok_1(2)
- 8005637 to 8005652 labelled f_1(3), g_1(3)
- 8005637 to 8005671 labelled proper_1(4)
- 8005639 to 8005633 labelled mark_1(2)
- 8005639 to 8005645 labelled proper_1(3)
- 8005638 to 8005639 labelled f_1(2)
- 8005638 to 8005646 labelled proper_1(3)
- 8005640 to 8005633 labelled f_1(2)
- 8005641 to 8005633 labelled g_1(2)
- 8005642 to 8005640 labelled g_1(2)
- 8005643 to 8005633 labelled g_1(3)
- 8005644 to 8005629 labelled ok_1(2)
- 8005644 to 8005647 labelled g_1(2), f_1(2)
- 8005644 to 8005633 labelled ok_1(2)
- 8005644 to 8005645 labelled active_1(3)
- 8005644 to 8005660 labelled g_1(3)
- 8005644 to 8005656 labelled proper_1(4)
- 8005644 to 8005664 labelled proper_1(3)
- 8005645 to 8005617 labelled top_1(3)
- 8005646 to 8005645 labelled f_1(3)
- 8005647 to 8005625 labelled ok_1(2)
- 8005647 to 8005643 labelled ok_1(2)
- 8005647 to 8005633 labelled active_1(2)
- 8005647 to 8005648 labelled ok_1(2)
- 8005647 to 8005651 labelled g_1(3), f_1(3)
- 8005647 to 8005655 labelled f_1(3), g_1(3)
- 8005647 to 8005659 labelled g_1(4)
- 8005647 to 8005662 labelled proper_1(5)
- 8005647 to 8005666 labelled proper_1(4)
- 8005648 to 8005643 labelled g_1(2), f_1(2)
- 8005648 to 8005648 labelled f_1(2), g_1(2)
- 8005649 to 8005640 labelled ok_1(3)
- 8005649 to 8005651 labelled f_1(3)
- 8005649 to 8005645 labelled ok_1(3)
- 8005649 to 8005661 labelled active_1(4), ok_1(3)
- 8005649 to 8005664 labelled ok_1(3)
- 8005649 to 8005656 labelled ok_1(3)
- 8005649 to 8005658 labelled g_1(4)
- 8005649 to 8005669 labelled f_1(4), g_1(4)
- 8005649 to 8005654 labelled g_1(4)
- 8005649 to 8005663 labelled g_1(5)
- 8005649 to 8005667 labelled proper_1(6)
- 8005650 to 8005646 labelled g_1(3)
- 8005651 to 8005633 labelled ok_1(3)
- 8005651 to 8005643 labelled ok_1(3)
- 8005651 to 8005645 labelled active_1(3)
- 8005651 to 8005657 labelled g_1(4)
- 8005652 to 8005650 labelled ok_1(3)
- 8005652 to 8005654 labelled g_1(4)
- 8005652 to 8005663 labelled g_1(5)
- 8005652 to 8005662 labelled ok_1(3)
- 8005652 to 8005667 labelled proper_1(6)
- 8005652 to 8005666 labelled ok_1(3)
- 8005652 to 8005669 labelled f_1(4), g_1(4)
- 8005652 to 8005671 labelled ok_1(3)
- 8005652 to 8005668 labelled g_1(4), f_1(4)
- 8005653 to 8005633 labelled mark_1(3)
- 8005653 to 8005645 labelled proper_1(3)
- 8005654 to 8005646 labelled ok_1(4)
- 8005654 to 8005658 labelled f_1(4)
- 8005654 to 8005661 labelled ok_1(4)
- 8005654 to 8005665 labelled active_1(5)
- 8005655 to 8005648 labelled ok_1(3)
- 8005655 to 8005651 labelled g_1(3), f_1(3)
- 8005655 to 8005655 labelled f_1(3), g_1(3)
- 8005655 to 8005659 labelled g_1(4)
- 8005655 to 8005662 labelled proper_1(5)
- 8005655 to 8005666 labelled proper_1(4)
- 8005656 to 8005645 labelled g_1(4)
- 8005656 to 8005661 labelled g_1(4)
- 8005657 to 8005633 labelled ok_1(4)
- 8005657 to 8005645 labelled active_1(3)
- 8005658 to 8005645 labelled ok_1(4)
- 8005658 to 8005661 labelled active_1(4)
- 8005658 to 8005664 labelled ok_1(4)
- 8005658 to 8005656 labelled ok_1(4)
- 8005658 to 8005674 labelled g_1(5)
- 8005658 to 8005658 labelled g_1(4)
- 8005658 to 8005669 labelled f_1(4), g_1(4)
- 8005658 to 8005672 labelled g_1(5)
- 8005659 to 8005645 labelled mark_1(4)
- 8005659 to 8005661 labelled proper_1(4)
- 8005660 to 8005645 labelled mark_1(3)
- 8005660 to 8005661 labelled proper_1(4)
- 8005661 to 8005617 labelled top_1(4)
- 8005662 to 8005661 labelled g_1(5)
- 8005663 to 8005661 labelled mark_1(5)
- 8005663 to 8005665 labelled proper_1(5)
- 8005664 to 8005656 labelled g_1(3)
- 8005664 to 8005662 labelled f_1(3), g_1(3)
- 8005664 to 8005666 labelled f_1(3), g_1(3)
- 8005664 to 8005664 labelled g_1(3)
- 8005665 to 8005617 labelled top_1(5)
- 8005666 to 8005662 labelled g_1(4), f_1(4)
- 8005666 to 8005666 labelled g_1(4), f_1(4)
- 8005667 to 8005665 labelled g_1(6)
- 8005668 to 8005667 labelled ok_1(4)
- 8005668 to 8005670 labelled g_1(5)
- 8005669 to 8005662 labelled ok_1(4)
- 8005669 to 8005666 labelled ok_1(4)
- 8005669 to 8005672 labelled g_1(5)
- 8005669 to 8005675 labelled f_1(5), g_1(5)
- 8005670 to 8005665 labelled ok_1(5)
- 8005670 to 8005673 labelled active_1(6)
- 8005671 to 8005667 labelled f_1(4), g_1(4)
- 8005672 to 8005661 labelled ok_1(5)
- 8005672 to 8005665 labelled active_1(5)
- 8005673 to 8005617 labelled top_1(6)
- 8005674 to 8005645 labelled ok_1(5)
- 8005674 to 8005661 labelled active_1(4)
- 8005675 to 8005662 labelled ok_1(5)
- 8005675 to 8005666 labelled ok_1(5)
- 8005675 to 8005676 labelled g_1(6)
- 8005675 to 8005675 labelled f_1(5), g_1(5)
- 8005676 to 8005661 labelled ok_1(6)
- 8005676 to 8005665 labelled active_1(5)