(3) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 4. This implies Q-termination of R.
The following rules were used to construct the certificate:
b(a(b(a(a(x))))) → a(a(a(b(a(b(a(b(x))))))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
6, 8, 9, 10, 11, 12, 13, 14, 15, 25, 27, 29, 31, 33, 35, 37, 173, 174, 175, 176, 178, 179, 181, 194, 195, 196, 197, 198, 199, 200, 206, 207, 208, 209, 210, 211, 212, 222, 223, 224, 225, 226, 227, 228, 236, 237, 238, 239, 240, 241, 242, 264, 265, 266, 267, 268, 269, 270, 271, 272, 273, 274, 275, 276, 277, 285, 286, 287, 288, 289, 290, 291
Node 6 is start node and node 8 is final node.
Those nodes are connected through the following edges:
- 6 to 9 labelled a_1(0)
- 8 to 8 labelled #_1(0)
- 9 to 10 labelled a_1(0)
- 10 to 11 labelled a_1(0)
- 11 to 12 labelled b_1(0)
- 11 to 173 labelled a_1(1)
- 12 to 13 labelled a_1(0)
- 13 to 14 labelled b_1(0)
- 13 to 25 labelled a_1(1)
- 14 to 15 labelled a_1(0)
- 15 to 8 labelled b_1(0)
- 15 to 25 labelled a_1(1)
- 25 to 27 labelled a_1(1)
- 27 to 29 labelled a_1(1)
- 29 to 31 labelled b_1(1)
- 29 to 194 labelled a_1(2)
- 31 to 33 labelled a_1(1)
- 33 to 35 labelled b_1(1)
- 33 to 25 labelled a_1(1)
- 35 to 37 labelled a_1(1)
- 37 to 8 labelled b_1(1)
- 37 to 25 labelled a_1(1)
- 173 to 174 labelled a_1(1)
- 174 to 175 labelled a_1(1)
- 175 to 176 labelled b_1(1)
- 176 to 178 labelled a_1(1)
- 178 to 179 labelled b_1(1)
- 178 to 206 labelled a_1(2)
- 179 to 181 labelled a_1(1)
- 181 to 25 labelled b_1(1)
- 194 to 195 labelled a_1(2)
- 195 to 196 labelled a_1(2)
- 196 to 197 labelled b_1(2)
- 197 to 198 labelled a_1(2)
- 198 to 199 labelled b_1(2)
- 198 to 206 labelled a_1(2)
- 199 to 200 labelled a_1(2)
- 200 to 25 labelled b_1(2)
- 206 to 207 labelled a_1(2)
- 207 to 208 labelled a_1(2)
- 208 to 209 labelled b_1(2)
- 209 to 210 labelled a_1(2)
- 210 to 211 labelled b_1(2)
- 210 to 222 labelled a_1(3)
- 211 to 212 labelled a_1(2)
- 212 to 29 labelled b_1(2)
- 222 to 223 labelled a_1(3)
- 223 to 224 labelled a_1(3)
- 224 to 225 labelled b_1(3)
- 224 to 264 labelled a_1(4)
- 225 to 226 labelled a_1(3)
- 226 to 227 labelled b_1(3)
- 227 to 228 labelled a_1(3)
- 228 to 195 labelled b_1(3)
- 228 to 236 labelled a_1(3)
- 236 to 237 labelled a_1(3)
- 237 to 238 labelled a_1(3)
- 238 to 239 labelled b_1(3)
- 239 to 240 labelled a_1(3)
- 240 to 241 labelled b_1(3)
- 240 to 271 labelled a_1(3)
- 241 to 242 labelled a_1(3)
- 242 to 206 labelled b_1(3)
- 264 to 265 labelled a_1(4)
- 265 to 266 labelled a_1(4)
- 266 to 267 labelled b_1(4)
- 267 to 268 labelled a_1(4)
- 268 to 269 labelled b_1(4)
- 268 to 285 labelled a_1(4)
- 269 to 270 labelled a_1(4)
- 270 to 236 labelled b_1(4)
- 271 to 272 labelled a_1(3)
- 272 to 273 labelled a_1(3)
- 273 to 274 labelled b_1(3)
- 274 to 275 labelled a_1(3)
- 275 to 276 labelled b_1(3)
- 276 to 277 labelled a_1(3)
- 277 to 208 labelled b_1(3)
- 285 to 286 labelled a_1(4)
- 286 to 287 labelled a_1(4)
- 287 to 288 labelled b_1(4)
- 288 to 289 labelled a_1(4)
- 289 to 290 labelled b_1(4)
- 290 to 291 labelled a_1(4)
- 291 to 238 labelled b_1(4)