(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:
1529270, 1529271, 1529272, 1529273, 1529274, 1529275, 1529276, 1529277, 1529278, 1529279, 1529280, 1529281, 1529282, 1529284, 1529285, 1529283, 1529286, 1529287, 1529288, 1529289, 1529290, 1529291, 1529292, 1529294, 1529295, 1529293, 1529296, 1529297, 1529298, 1529299, 1529300, 1529301, 1529302, 1529303, 1529304, 1529305, 1529306, 1529307, 1529308, 1529309, 1529310, 1529311, 1529312, 1529313, 1529314, 1529315, 1529316, 1529317, 1529318, 1529319, 1529320, 1529321, 1529322, 1529323
Node 1529270 is start node and node 1529271 is final node.
Those nodes are connect through the following edges:
- 1529270 to 1529272 labelled proper_1(0)
- 1529270 to 1529273 labelled active_1(0), proper_1(0)
- 1529270 to 1529274 labelled g_1(0), f_1(0), c'_1(0)
- 1529270 to 1529275 labelled c'_1(0)
- 1529270 to 1529283 labelled c'_1(1)
- 1529270 to 1529286 labelled proper_1(1)
- 1529270 to 1529282 labelled proper_1(1)
- 1529270 to 1529285 labelled g_1(1)
- 1529270 to 1529292 labelled proper_1(2)
- 1529270 to 1529293 labelled c'_1(2)
- 1529270 to 1529305 labelled c'_1(3)
- 1529270 to 1529321 labelled c'_1(4)
- 1529271 to 1529271 labelled #_1(0)
- 1529272 to 1529271 labelled g_1(0), f_1(0)
- 1529272 to 1529278 labelled proper_1(1)
- 1529272 to 1529281 labelled g_1(1)
- 1529272 to 1529287 labelled proper_1(2)
- 1529273 to 1529271 labelled top_1(0)
- 1529274 to 1529271 labelled ok_1(0), mark_1(0)
- 1529274 to 1529279 labelled proper_1(1), active_1(1)
- 1529274 to 1529280 labelled g_1(1), f_1(1)
- 1529274 to 1529290 labelled g_1(2)
- 1529274 to 1529297 labelled proper_1(3)
- 1529274 to 1529300 labelled proper_1(2)
- 1529275 to 1529276 labelled g_1(0)
- 1529275 to 1529288 labelled proper_1(1)
- 1529276 to 1529277 labelled f_1(0)
- 1529276 to 1529282 labelled proper_1(1)
- 1529277 to 1529271 labelled mark_1(0)
- 1529277 to 1529279 labelled proper_1(1)
- 1529278 to 1529271 labelled f_1(1), g_1(1)
- 1529278 to 1529278 labelled proper_1(1)
- 1529278 to 1529281 labelled g_1(1)
- 1529278 to 1529287 labelled proper_1(2)
- 1529279 to 1529271 labelled top_1(1)
- 1529280 to 1529271 labelled ok_1(1)
- 1529280 to 1529279 labelled active_1(1)
- 1529280 to 1529280 labelled g_1(1), f_1(1)
- 1529280 to 1529290 labelled g_1(2)
- 1529280 to 1529297 labelled proper_1(3)
- 1529280 to 1529300 labelled proper_1(2)
- 1529281 to 1529271 labelled mark_1(1)
- 1529281 to 1529279 labelled proper_1(1)
- 1529282 to 1529279 labelled f_1(1)
- 1529284 to 1529285 labelled f_1(1)
- 1529284 to 1529291 labelled proper_1(2)
- 1529285 to 1529279 labelled mark_1(1)
- 1529285 to 1529289 labelled proper_1(2)
- 1529283 to 1529284 labelled g_1(1)
- 1529283 to 1529279 labelled ok_1(1)
- 1529283 to 1529289 labelled active_1(2)
- 1529283 to 1529288 labelled ok_1(1)
- 1529283 to 1529296 labelled g_1(2), f_1(2)
- 1529283 to 1529299 labelled proper_1(2)
- 1529283 to 1529297 labelled ok_1(1)
- 1529283 to 1529300 labelled ok_1(1)
- 1529283 to 1529306 labelled f_1(2), g_1(2)
- 1529283 to 1529308 labelled g_1(3)
- 1529283 to 1529313 labelled proper_1(4)
- 1529286 to 1529279 labelled g_1(1)
- 1529286 to 1529297 labelled g_1(1), f_1(1)
- 1529286 to 1529300 labelled f_1(1), g_1(1)
- 1529287 to 1529279 labelled g_1(2)
- 1529288 to 1529282 labelled g_1(1)
- 1529289 to 1529271 labelled top_1(2)
- 1529290 to 1529279 labelled mark_1(2)
- 1529290 to 1529289 labelled proper_1(2)
- 1529291 to 1529289 labelled f_1(2)
- 1529292 to 1529289 labelled g_1(2)
- 1529294 to 1529295 labelled f_1(2)
- 1529294 to 1529302 labelled proper_1(3)
- 1529295 to 1529289 labelled mark_1(2)
- 1529295 to 1529298 labelled proper_1(3)
- 1529293 to 1529294 labelled g_1(2)
- 1529293 to 1529299 labelled ok_1(2)
- 1529293 to 1529303 labelled g_1(3)
- 1529293 to 1529304 labelled proper_1(3)
- 1529293 to 1529315 labelled g_1(4)
- 1529293 to 1529313 labelled ok_1(2)
- 1529293 to 1529317 labelled proper_1(5)
- 1529296 to 1529282 labelled ok_1(2)
- 1529296 to 1529301 labelled f_1(2)
- 1529296 to 1529289 labelled ok_1(2)
- 1529296 to 1529297 labelled ok_1(2)
- 1529296 to 1529298 labelled active_1(3)
- 1529296 to 1529307 labelled g_1(3)
- 1529297 to 1529289 labelled g_1(3)
- 1529298 to 1529271 labelled top_1(3)
- 1529299 to 1529291 labelled g_1(2)
- 1529300 to 1529297 labelled f_1(2), g_1(2)
- 1529300 to 1529300 labelled f_1(2), g_1(2)
- 1529301 to 1529279 labelled ok_1(2)
- 1529301 to 1529289 labelled active_1(2)
- 1529302 to 1529298 labelled f_1(3)
- 1529303 to 1529291 labelled ok_1(3)
- 1529303 to 1529307 labelled f_1(3)
- 1529303 to 1529298 labelled ok_1(3)
- 1529303 to 1529316 labelled active_1(4)
- 1529304 to 1529302 labelled g_1(3)
- 1529305 to 1529304 labelled ok_1(3)
- 1529305 to 1529310 labelled g_1(4)
- 1529305 to 1529318 labelled g_1(5)
- 1529305 to 1529317 labelled ok_1(3)
- 1529305 to 1529320 labelled proper_1(6)
- 1529306 to 1529300 labelled ok_1(2)
- 1529306 to 1529309 labelled g_1(3), f_1(3)
- 1529306 to 1529311 labelled f_1(3), g_1(3)
- 1529307 to 1529289 labelled ok_1(3)
- 1529307 to 1529298 labelled active_1(3)
- 1529308 to 1529289 labelled mark_1(3)
- 1529308 to 1529298 labelled proper_1(3)
- 1529309 to 1529297 labelled ok_1(3)
- 1529309 to 1529312 labelled g_1(4)
- 1529310 to 1529302 labelled ok_1(4)
- 1529310 to 1529314 labelled f_1(4)
- 1529310 to 1529316 labelled ok_1(4)
- 1529310 to 1529319 labelled active_1(5)
- 1529311 to 1529300 labelled ok_1(3)
- 1529311 to 1529309 labelled g_1(3), f_1(3)
- 1529311 to 1529311 labelled f_1(3), g_1(3)
- 1529312 to 1529289 labelled ok_1(4)
- 1529312 to 1529298 labelled active_1(3)
- 1529313 to 1529298 labelled g_1(4)
- 1529314 to 1529298 labelled ok_1(4)
- 1529314 to 1529316 labelled active_1(4)
- 1529315 to 1529298 labelled mark_1(4)
- 1529315 to 1529316 labelled proper_1(4)
- 1529316 to 1529271 labelled top_1(4)
- 1529317 to 1529316 labelled g_1(5)
- 1529318 to 1529316 labelled mark_1(5)
- 1529318 to 1529319 labelled proper_1(5)
- 1529319 to 1529271 labelled top_1(5)
- 1529320 to 1529319 labelled g_1(6)
- 1529321 to 1529320 labelled ok_1(4)
- 1529321 to 1529322 labelled g_1(5)
- 1529322 to 1529319 labelled ok_1(5)
- 1529322 to 1529323 labelled active_1(6)
- 1529323 to 1529271 labelled top_1(6)