(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:
2343133, 2343134, 2343135, 2343136, 2343137, 2343139, 2343140, 2343138, 2343141, 2343142, 2343146, 2343143, 2343144, 2343145, 2343147, 2343148, 2343149, 2343150, 2343151, 2343152, 2343153, 2343154, 2343155, 2343156, 2343157, 2343158, 2343160, 2343161, 2343159, 2343162, 2343163, 2343164, 2343165, 2343166, 2343167, 2343168, 2343169, 2343170, 2343171, 2343172, 2343173, 2343174, 2343175, 2343176, 2343177, 2343178, 2343179, 2343180, 2343181, 2343182, 2343183, 2343184, 2343185, 2343186, 2343187
Node 2343133 is start node and node 2343134 is final node.
Those nodes are connect through the following edges:
- 2343133 to 2343135 labelled g_1(0), top_1(0)
- 2343133 to 2343136 labelled ok_1(0), mark_1(0)
- 2343133 to 2343137 labelled mark_1(0)
- 2343133 to 2343141 labelled top_1(0), g_1(0), f_1(0)
- 2343133 to 2343140 labelled ok_1(0)
- 2343133 to 2343149 labelled top_1(1)
- 2343133 to 2343150 labelled ok_1(1)
- 2343133 to 2343145 labelled ok_1(1)
- 2343133 to 2343151 labelled mark_1(1)
- 2343133 to 2343164 labelled top_1(2)
- 2343133 to 2343182 labelled top_1(3)
- 2343134 to 2343134 labelled #_1(0)
- 2343135 to 2343134 labelled active_1(0)
- 2343135 to 2343142 labelled g_1(1)
- 2343135 to 2343143 labelled mark_1(1)
- 2343135 to 2343154 labelled mark_1(2)
- 2343136 to 2343134 labelled g_1(0), f_1(0)
- 2343136 to 2343147 labelled ok_1(1), mark_1(1)
- 2343137 to 2343138 labelled f_1(0)
- 2343139 to 2343140 labelled f_1(0)
- 2343140 to 2343134 labelled a(0)
- 2343138 to 2343139 labelled g_1(0)
- 2343141 to 2343134 labelled proper_1(0)
- 2343141 to 2343148 labelled g_1(1), f_1(1)
- 2343141 to 2343146 labelled ok_1(1)
- 2343141 to 2343153 labelled ok_1(2)
- 2343141 to 2343152 labelled ok_1(2)
- 2343142 to 2343134 labelled active_1(1)
- 2343142 to 2343142 labelled g_1(1)
- 2343142 to 2343143 labelled mark_1(1)
- 2343142 to 2343154 labelled mark_1(2)
- 2343146 to 2343134 labelled a(1)
- 2343143 to 2343144 labelled f_1(1)
- 2343144 to 2343145 labelled g_1(1)
- 2343145 to 2343146 labelled f_1(1)
- 2343147 to 2343134 labelled f_1(1), g_1(1)
- 2343147 to 2343147 labelled ok_1(1), mark_1(1)
- 2343148 to 2343134 labelled proper_1(1)
- 2343148 to 2343148 labelled g_1(1), f_1(1)
- 2343148 to 2343146 labelled ok_1(1)
- 2343148 to 2343152 labelled ok_1(2)
- 2343148 to 2343153 labelled ok_1(2)
- 2343149 to 2343146 labelled active_1(1)
- 2343149 to 2343143 labelled proper_1(1)
- 2343149 to 2343155 labelled f_1(2)
- 2343149 to 2343152 labelled active_1(1)
- 2343149 to 2343154 labelled proper_1(1)
- 2343149 to 2343153 labelled active_1(1)
- 2343149 to 2343158 labelled g_1(2)
- 2343149 to 2343159 labelled mark_1(2)
- 2343149 to 2343167 labelled mark_1(3)
- 2343149 to 2343173 labelled ok_1(3)
- 2343150 to 2343146 labelled g_1(1)
- 2343150 to 2343152 labelled g_1(1), f_1(1)
- 2343150 to 2343153 labelled g_1(1), f_1(1)
- 2343151 to 2343143 labelled g_1(1)
- 2343151 to 2343154 labelled g_1(1)
- 2343152 to 2343146 labelled g_1(2)
- 2343152 to 2343152 labelled g_1(2)
- 2343152 to 2343153 labelled g_1(2)
- 2343153 to 2343146 labelled f_1(2)
- 2343153 to 2343152 labelled f_1(2)
- 2343153 to 2343153 labelled f_1(2)
- 2343154 to 2343143 labelled g_1(2)
- 2343154 to 2343154 labelled g_1(2)
- 2343155 to 2343144 labelled proper_1(2)
- 2343155 to 2343156 labelled g_1(2)
- 2343155 to 2343169 labelled ok_1(3)
- 2343156 to 2343145 labelled proper_1(2)
- 2343156 to 2343157 labelled f_1(2)
- 2343156 to 2343166 labelled ok_1(3)
- 2343157 to 2343146 labelled proper_1(2)
- 2343157 to 2343162 labelled ok_1(2)
- 2343158 to 2343143 labelled proper_1(2)
- 2343158 to 2343146 labelled active_1(2)
- 2343158 to 2343153 labelled active_1(2)
- 2343158 to 2343154 labelled proper_1(2)
- 2343158 to 2343152 labelled active_1(2)
- 2343158 to 2343163 labelled g_1(3)
- 2343158 to 2343155 labelled f_1(2)
- 2343158 to 2343159 labelled mark_1(2)
- 2343158 to 2343167 labelled mark_1(3)
- 2343158 to 2343170 labelled mark_1(4)
- 2343158 to 2343173 labelled ok_1(3)
- 2343158 to 2343174 labelled ok_1(4)
- 2343160 to 2343161 labelled g_1(2)
- 2343161 to 2343162 labelled f_1(2)
- 2343159 to 2343160 labelled f_1(2)
- 2343162 to 2343134 labelled a(2)
- 2343163 to 2343143 labelled proper_1(3)
- 2343163 to 2343146 labelled active_1(3)
- 2343163 to 2343153 labelled active_1(3)
- 2343163 to 2343154 labelled proper_1(3)
- 2343163 to 2343152 labelled active_1(3)
- 2343163 to 2343163 labelled g_1(3)
- 2343163 to 2343155 labelled f_1(2)
- 2343163 to 2343159 labelled mark_1(2)
- 2343163 to 2343167 labelled mark_1(3)
- 2343163 to 2343170 labelled mark_1(4)
- 2343163 to 2343173 labelled ok_1(3)
- 2343163 to 2343174 labelled ok_1(4)
- 2343164 to 2343159 labelled proper_1(2)
- 2343164 to 2343165 labelled f_1(3)
- 2343164 to 2343167 labelled proper_1(2)
- 2343164 to 2343171 labelled g_1(3)
- 2343164 to 2343173 labelled active_1(2)
- 2343164 to 2343180 labelled ok_1(4)
- 2343165 to 2343160 labelled proper_1(3)
- 2343165 to 2343168 labelled g_1(3)
- 2343165 to 2343179 labelled ok_1(4)
- 2343166 to 2343162 labelled f_1(3)
- 2343167 to 2343159 labelled g_1(3)
- 2343167 to 2343167 labelled g_1(3)
- 2343167 to 2343170 labelled g_1(3)
- 2343168 to 2343161 labelled proper_1(3)
- 2343168 to 2343172 labelled f_1(3)
- 2343168 to 2343177 labelled ok_1(4)
- 2343169 to 2343166 labelled g_1(3)
- 2343170 to 2343167 labelled g_1(4)
- 2343170 to 2343170 labelled g_1(4)
- 2343171 to 2343159 labelled proper_1(3)
- 2343171 to 2343165 labelled f_1(3)
- 2343171 to 2343167 labelled proper_1(3)
- 2343171 to 2343176 labelled g_1(4)
- 2343171 to 2343173 labelled active_1(3)
- 2343171 to 2343170 labelled proper_1(3)
- 2343171 to 2343174 labelled active_1(3)
- 2343171 to 2343180 labelled ok_1(4)
- 2343171 to 2343181 labelled ok_1(5)
- 2343172 to 2343162 labelled proper_1(3)
- 2343172 to 2343175 labelled ok_1(3)
- 2343173 to 2343169 labelled f_1(3)
- 2343173 to 2343173 labelled g_1(3)
- 2343173 to 2343174 labelled g_1(3)
- 2343174 to 2343173 labelled g_1(4)
- 2343174 to 2343174 labelled g_1(4)
- 2343175 to 2343134 labelled a(3)
- 2343176 to 2343159 labelled proper_1(4)
- 2343176 to 2343167 labelled proper_1(4)
- 2343176 to 2343170 labelled proper_1(4)
- 2343176 to 2343176 labelled g_1(4)
- 2343176 to 2343165 labelled f_1(3)
- 2343176 to 2343178 labelled g_1(5)
- 2343176 to 2343174 labelled active_1(4)
- 2343176 to 2343173 labelled active_1(4)
- 2343176 to 2343180 labelled ok_1(4)
- 2343176 to 2343181 labelled ok_1(5)
- 2343176 to 2343184 labelled ok_1(6)
- 2343177 to 2343175 labelled f_1(4)
- 2343178 to 2343167 labelled proper_1(5)
- 2343178 to 2343170 labelled proper_1(5)
- 2343178 to 2343176 labelled g_1(4)
- 2343178 to 2343178 labelled g_1(5)
- 2343178 to 2343174 labelled active_1(5)
- 2343178 to 2343173 labelled active_1(5)
- 2343178 to 2343181 labelled ok_1(5)
- 2343178 to 2343184 labelled ok_1(6)
- 2343179 to 2343177 labelled g_1(4)
- 2343180 to 2343179 labelled f_1(4)
- 2343180 to 2343180 labelled g_1(4)
- 2343180 to 2343181 labelled g_1(4)
- 2343181 to 2343180 labelled g_1(5)
- 2343181 to 2343181 labelled g_1(5)
- 2343181 to 2343184 labelled g_1(5)
- 2343182 to 2343180 labelled active_1(3)
- 2343182 to 2343183 labelled g_1(4)
- 2343183 to 2343180 labelled active_1(4)
- 2343183 to 2343185 labelled g_1(5)
- 2343183 to 2343181 labelled active_1(4)
- 2343184 to 2343181 labelled g_1(6)
- 2343184 to 2343184 labelled g_1(6)
- 2343185 to 2343180 labelled active_1(5)
- 2343185 to 2343181 labelled active_1(5)
- 2343185 to 2343185 labelled g_1(5)
- 2343185 to 2343186 labelled g_1(6)
- 2343185 to 2343184 labelled active_1(5)
- 2343186 to 2343184 labelled active_1(6)
- 2343186 to 2343180 labelled active_1(6)
- 2343186 to 2343181 labelled active_1(6)
- 2343186 to 2343185 labelled g_1(5)
- 2343186 to 2343186 labelled g_1(6)
- 2343186 to 2343187 labelled g_1(7)
- 2343187 to 2343181 labelled active_1(7)
- 2343187 to 2343184 labelled active_1(7)
- 2343187 to 2343186 labelled g_1(6)
- 2343187 to 2343187 labelled g_1(7)