(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(g(X)) → g(active(X))
g(mark(X)) → mark(g(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:
8871101, 8871102, 8871103, 8871104, 8871105, 8871107, 8871108, 8871106, 8871109, 8871110, 8871111, 8871112, 8871113, 8871114, 8871115, 8871116, 8871117, 8871118, 8871119, 8871120, 8871121, 8871122, 8871123, 8871124, 8871125, 8871126, 8871127, 8871129, 8871128, 8871130, 8871131, 8871132, 8871133, 8871134, 8871135, 8871136, 8871137, 8871138, 8871139, 8871140, 8871141, 8871142, 8871143, 8871144, 8871145, 8871146, 8871147, 8871148, 8871149, 8871150, 8871151, 8871152, 8871153, 8871154
Node 8871101 is start node and node 8871102 is final node.
Those nodes are connect through the following edges:
- 8871101 to 8871103 labelled g_1(0), top_1(0)
- 8871101 to 8871104 labelled ok_1(0), mark_1(0)
- 8871101 to 8871105 labelled mark_1(0)
- 8871101 to 8871109 labelled top_1(0), g_1(0), f_1(0)
- 8871101 to 8871108 labelled ok_1(0)
- 8871101 to 8871117 labelled top_1(1)
- 8871101 to 8871118 labelled ok_1(1)
- 8871101 to 8871114 labelled ok_1(1)
- 8871101 to 8871119 labelled mark_1(1)
- 8871101 to 8871131 labelled top_1(2)
- 8871101 to 8871148 labelled top_1(3)
- 8871102 to 8871102 labelled #_1(0)
- 8871103 to 8871102 labelled active_1(0)
- 8871103 to 8871111 labelled g_1(1)
- 8871103 to 8871112 labelled mark_1(1)
- 8871103 to 8871121 labelled mark_1(2)
- 8871104 to 8871102 labelled g_1(0), f_1(0)
- 8871104 to 8871110 labelled ok_1(1), mark_1(1)
- 8871105 to 8871106 labelled f_1(0)
- 8871107 to 8871108 labelled f_1(0)
- 8871108 to 8871102 labelled a(0)
- 8871106 to 8871107 labelled g_1(0)
- 8871109 to 8871102 labelled proper_1(0)
- 8871109 to 8871116 labelled g_1(1), f_1(1)
- 8871109 to 8871115 labelled ok_1(1)
- 8871109 to 8871122 labelled ok_1(2)
- 8871110 to 8871102 labelled g_1(1), f_1(1)
- 8871110 to 8871110 labelled ok_1(1), mark_1(1)
- 8871111 to 8871102 labelled active_1(1)
- 8871111 to 8871111 labelled g_1(1)
- 8871111 to 8871112 labelled mark_1(1)
- 8871111 to 8871121 labelled mark_1(2)
- 8871112 to 8871113 labelled f_1(1)
- 8871113 to 8871114 labelled g_1(1)
- 8871114 to 8871115 labelled f_1(1)
- 8871115 to 8871102 labelled a(1)
- 8871116 to 8871102 labelled proper_1(1)
- 8871116 to 8871116 labelled g_1(1), f_1(1)
- 8871116 to 8871115 labelled ok_1(1)
- 8871116 to 8871122 labelled ok_1(2)
- 8871117 to 8871115 labelled active_1(1)
- 8871117 to 8871112 labelled proper_1(1)
- 8871117 to 8871120 labelled f_1(2)
- 8871117 to 8871122 labelled active_1(1)
- 8871117 to 8871121 labelled proper_1(1)
- 8871117 to 8871124 labelled g_1(2)
- 8871117 to 8871126 labelled mark_1(2)
- 8871117 to 8871133 labelled mark_1(3)
- 8871117 to 8871139 labelled ok_1(3)
- 8871118 to 8871115 labelled g_1(1)
- 8871118 to 8871122 labelled g_1(1), f_1(1)
- 8871119 to 8871112 labelled g_1(1)
- 8871119 to 8871121 labelled g_1(1)
- 8871120 to 8871113 labelled proper_1(2)
- 8871120 to 8871123 labelled g_1(2)
- 8871120 to 8871136 labelled ok_1(3)
- 8871121 to 8871112 labelled g_1(2)
- 8871121 to 8871121 labelled g_1(2)
- 8871122 to 8871115 labelled g_1(2), f_1(2)
- 8871122 to 8871122 labelled g_1(2), f_1(2)
- 8871123 to 8871114 labelled proper_1(2)
- 8871123 to 8871125 labelled f_1(2)
- 8871123 to 8871134 labelled ok_1(3)
- 8871124 to 8871122 labelled active_1(2)
- 8871124 to 8871121 labelled proper_1(2)
- 8871124 to 8871112 labelled proper_1(2)
- 8871124 to 8871115 labelled active_1(2)
- 8871124 to 8871130 labelled g_1(3)
- 8871124 to 8871120 labelled f_1(2)
- 8871124 to 8871126 labelled mark_1(2)
- 8871124 to 8871133 labelled mark_1(3)
- 8871124 to 8871139 labelled ok_1(3)
- 8871124 to 8871140 labelled mark_1(4)
- 8871124 to 8871142 labelled ok_1(4)
- 8871125 to 8871115 labelled proper_1(2)
- 8871125 to 8871129 labelled ok_1(2)
- 8871126 to 8871127 labelled f_1(2)
- 8871127 to 8871128 labelled g_1(2)
- 8871129 to 8871102 labelled a(2)
- 8871128 to 8871129 labelled f_1(2)
- 8871130 to 8871122 labelled active_1(3)
- 8871130 to 8871121 labelled proper_1(3)
- 8871130 to 8871112 labelled proper_1(3)
- 8871130 to 8871115 labelled active_1(3)
- 8871130 to 8871130 labelled g_1(3)
- 8871130 to 8871120 labelled f_1(2)
- 8871130 to 8871126 labelled mark_1(2)
- 8871130 to 8871133 labelled mark_1(3)
- 8871130 to 8871139 labelled ok_1(3)
- 8871130 to 8871140 labelled mark_1(4)
- 8871130 to 8871142 labelled ok_1(4)
- 8871131 to 8871126 labelled proper_1(2)
- 8871131 to 8871132 labelled f_1(3)
- 8871131 to 8871133 labelled proper_1(2)
- 8871131 to 8871138 labelled g_1(3)
- 8871131 to 8871139 labelled active_1(2)
- 8871131 to 8871147 labelled ok_1(4)
- 8871132 to 8871127 labelled proper_1(3)
- 8871132 to 8871135 labelled g_1(3)
- 8871132 to 8871146 labelled ok_1(4)
- 8871133 to 8871126 labelled g_1(3)
- 8871133 to 8871133 labelled g_1(3)
- 8871133 to 8871140 labelled g_1(3)
- 8871134 to 8871129 labelled f_1(3)
- 8871135 to 8871128 labelled proper_1(3)
- 8871135 to 8871137 labelled f_1(3)
- 8871135 to 8871143 labelled ok_1(4)
- 8871136 to 8871134 labelled g_1(3)
- 8871137 to 8871129 labelled proper_1(3)
- 8871137 to 8871141 labelled ok_1(3)
- 8871138 to 8871126 labelled proper_1(3)
- 8871138 to 8871133 labelled proper_1(3)
- 8871138 to 8871132 labelled f_1(3)
- 8871138 to 8871139 labelled active_1(3)
- 8871138 to 8871140 labelled proper_1(3)
- 8871138 to 8871144 labelled g_1(4)
- 8871138 to 8871142 labelled active_1(3)
- 8871138 to 8871147 labelled ok_1(4)
- 8871138 to 8871149 labelled ok_1(5)
- 8871139 to 8871136 labelled f_1(3)
- 8871139 to 8871139 labelled g_1(3)
- 8871139 to 8871142 labelled g_1(3)
- 8871140 to 8871133 labelled g_1(4)
- 8871140 to 8871140 labelled g_1(4)
- 8871141 to 8871102 labelled a(3)
- 8871142 to 8871139 labelled g_1(4)
- 8871142 to 8871142 labelled g_1(4)
- 8871143 to 8871141 labelled f_1(4)
- 8871144 to 8871140 labelled proper_1(4)
- 8871144 to 8871133 labelled proper_1(4)
- 8871144 to 8871126 labelled proper_1(4)
- 8871144 to 8871144 labelled g_1(4)
- 8871144 to 8871145 labelled g_1(5)
- 8871144 to 8871139 labelled active_1(4)
- 8871144 to 8871132 labelled f_1(3)
- 8871144 to 8871142 labelled active_1(4)
- 8871144 to 8871147 labelled ok_1(4)
- 8871144 to 8871149 labelled ok_1(5)
- 8871144 to 8871151 labelled ok_1(6)
- 8871145 to 8871133 labelled proper_1(5)
- 8871145 to 8871140 labelled proper_1(5)
- 8871145 to 8871144 labelled g_1(4)
- 8871145 to 8871145 labelled g_1(5)
- 8871145 to 8871142 labelled active_1(5)
- 8871145 to 8871139 labelled active_1(5)
- 8871145 to 8871149 labelled ok_1(5)
- 8871145 to 8871151 labelled ok_1(6)
- 8871146 to 8871143 labelled g_1(4)
- 8871147 to 8871146 labelled f_1(4)
- 8871147 to 8871147 labelled g_1(4)
- 8871147 to 8871149 labelled g_1(4)
- 8871148 to 8871147 labelled active_1(3)
- 8871148 to 8871150 labelled g_1(4)
- 8871149 to 8871147 labelled g_1(5)
- 8871149 to 8871149 labelled g_1(5)
- 8871149 to 8871151 labelled g_1(5)
- 8871150 to 8871147 labelled active_1(4)
- 8871150 to 8871152 labelled g_1(5)
- 8871150 to 8871149 labelled active_1(4)
- 8871151 to 8871149 labelled g_1(6)
- 8871151 to 8871151 labelled g_1(6)
- 8871152 to 8871147 labelled active_1(5)
- 8871152 to 8871149 labelled active_1(5)
- 8871152 to 8871153 labelled g_1(6)
- 8871152 to 8871152 labelled g_1(5)
- 8871152 to 8871151 labelled active_1(5)
- 8871153 to 8871147 labelled active_1(6)
- 8871153 to 8871149 labelled active_1(6)
- 8871153 to 8871151 labelled active_1(6)
- 8871153 to 8871153 labelled g_1(6)
- 8871153 to 8871152 labelled g_1(5)
- 8871153 to 8871154 labelled g_1(7)
- 8871154 to 8871151 labelled active_1(7)
- 8871154 to 8871149 labelled active_1(7)
- 8871154 to 8871153 labelled g_1(6)
- 8871154 to 8871154 labelled g_1(7)