(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:
a'(f(f(active(x)))) → a'(f(g(f(mark(x)))))
g(active(X)) → active(g(X))
mark(g(X)) → g(mark(X))
f(proper(X)) → proper(f(X))
a'(proper(x)) → a'(ok(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:
2, 3, 5, 6, 7, 8, 9, 10, 18, 20, 25, 26, 27, 30, 31, 40, 41, 42, 43, 44, 45, 48, 49, 59, 62, 64, 65, 66, 67, 68, 69, 72, 75, 79, 81, 83, 86, 89, 90, 91, 94, 95, 98, 100
Node 2 is start node and node 3 is final node.
Those nodes are connected through the following edges:
- 2 to 5 labelled a'_1(0), f_1(0), g_1(0)
- 2 to 9 labelled active_1(0), proper_1(0)
- 2 to 8 labelled g_1(0)
- 2 to 10 labelled proper_1(0)
- 2 to 30 labelled active_1(1), proper_1(1)
- 2 to 42 labelled a'_1(1)
- 2 to 72 labelled a'_1(2)
- 3 to 3 labelled #_1(0)
- 5 to 6 labelled f_1(0)
- 5 to 3 labelled ok_1(0)
- 5 to 18 labelled f_1(1), g_1(1)
- 5 to 20 labelled active_1(1)
- 5 to 40 labelled active_1(2)
- 5 to 48 labelled proper_1(1)
- 6 to 7 labelled g_1(0)
- 6 to 41 labelled proper_1(1)
- 7 to 8 labelled f_1(0)
- 7 to 31 labelled proper_1(1)
- 8 to 3 labelled mark_1(0)
- 8 to 25 labelled g_1(1)
- 8 to 20 labelled proper_1(1)
- 8 to 40 labelled proper_1(2)
- 9 to 3 labelled g_1(0), top_1(0)
- 9 to 26 labelled active_1(1), proper_1(1)
- 10 to 3 labelled f_1(0)
- 10 to 27 labelled proper_1(1)
- 18 to 3 labelled ok_1(1)
- 18 to 18 labelled f_1(1), g_1(1)
- 18 to 20 labelled active_1(1)
- 18 to 40 labelled active_1(2)
- 20 to 3 labelled top_1(1)
- 25 to 3 labelled mark_1(1)
- 25 to 25 labelled g_1(1)
- 25 to 20 labelled proper_1(1)
- 25 to 40 labelled proper_1(2)
- 26 to 3 labelled g_1(1)
- 26 to 26 labelled active_1(1), proper_1(1)
- 27 to 3 labelled f_1(1)
- 27 to 27 labelled proper_1(1)
- 30 to 20 labelled g_1(1)
- 30 to 40 labelled g_1(1)
- 30 to 48 labelled f_1(1), g_1(1)
- 31 to 20 labelled f_1(1)
- 31 to 40 labelled f_1(1)
- 40 to 20 labelled g_1(2)
- 40 to 40 labelled g_1(2)
- 41 to 31 labelled g_1(1)
- 42 to 43 labelled f_1(1)
- 42 to 48 labelled ok_1(1)
- 42 to 64 labelled f_1(2)
- 42 to 67 labelled proper_1(2)
- 43 to 44 labelled g_1(1)
- 43 to 65 labelled proper_1(2)
- 44 to 45 labelled f_1(1)
- 44 to 59 labelled proper_1(2)
- 45 to 20 labelled mark_1(1)
- 45 to 49 labelled proper_1(2)
- 45 to 40 labelled mark_1(1)
- 45 to 62 labelled g_1(2)
- 45 to 68 labelled proper_1(3)
- 48 to 41 labelled f_1(1)
- 49 to 3 labelled top_1(2)
- 59 to 49 labelled f_1(2)
- 59 to 68 labelled f_1(2)
- 62 to 20 labelled mark_1(2)
- 62 to 40 labelled mark_1(2)
- 62 to 49 labelled proper_1(2)
- 62 to 66 labelled g_1(3)
- 62 to 68 labelled proper_1(3)
- 62 to 81 labelled proper_1(4)
- 64 to 41 labelled ok_1(2)
- 64 to 69 labelled g_1(2)
- 65 to 59 labelled g_1(2)
- 66 to 20 labelled mark_1(3)
- 66 to 40 labelled mark_1(3)
- 66 to 49 labelled proper_1(2)
- 66 to 66 labelled g_1(3)
- 66 to 68 labelled proper_1(3)
- 66 to 81 labelled proper_1(4)
- 67 to 65 labelled f_1(2)
- 68 to 49 labelled g_1(3)
- 68 to 68 labelled g_1(3)
- 68 to 81 labelled g_1(3)
- 69 to 31 labelled ok_1(2)
- 69 to 75 labelled f_1(2)
- 72 to 67 labelled ok_1(2)
- 72 to 83 labelled f_1(3)
- 75 to 20 labelled ok_1(2)
- 75 to 40 labelled ok_1(2)
- 75 to 49 labelled active_1(2)
- 75 to 79 labelled g_1(3)
- 75 to 68 labelled active_1(3)
- 75 to 81 labelled active_1(4)
- 79 to 20 labelled ok_1(3)
- 79 to 40 labelled ok_1(3)
- 79 to 49 labelled active_1(2)
- 79 to 79 labelled g_1(3)
- 79 to 68 labelled active_1(3)
- 79 to 81 labelled active_1(4)
- 81 to 68 labelled g_1(4)
- 81 to 81 labelled g_1(4)
- 83 to 65 labelled ok_1(3)
- 83 to 86 labelled g_1(3)
- 86 to 59 labelled ok_1(3)
- 86 to 89 labelled f_1(3)
- 89 to 49 labelled ok_1(3)
- 89 to 68 labelled ok_1(3)
- 89 to 90 labelled active_1(3)
- 89 to 91 labelled g_1(4)
- 89 to 95 labelled active_1(4)
- 89 to 98 labelled active_1(5)
- 90 to 3 labelled top_1(3)
- 91 to 49 labelled ok_1(4)
- 91 to 68 labelled ok_1(4)
- 91 to 81 labelled ok_1(4)
- 91 to 90 labelled active_1(3)
- 91 to 91 labelled g_1(4)
- 91 to 94 labelled g_1(5)
- 91 to 95 labelled active_1(4)
- 91 to 98 labelled active_1(5)
- 91 to 100 labelled active_1(6)
- 94 to 68 labelled ok_1(5)
- 94 to 81 labelled ok_1(5)
- 94 to 91 labelled g_1(4)
- 94 to 94 labelled g_1(5)
- 94 to 95 labelled active_1(4)
- 94 to 98 labelled active_1(5)
- 94 to 100 labelled active_1(6)
- 95 to 90 labelled g_1(4)
- 98 to 95 labelled g_1(5)
- 98 to 98 labelled g_1(5)
- 98 to 100 labelled g_1(5)
- 100 to 98 labelled g_1(6)
- 100 to 100 labelled g_1(6)