(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 2. This implies Q-termination of R.
The following rules were used to construct the certificate:
a(a(b(a(a(b(a(x))))))) → a(b(a(a(b(a(a(a(b(x)))))))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
3, 4, 6, 8, 10, 12, 14, 16, 17, 19, 41, 42, 43, 44, 45, 46, 47, 48, 276, 277, 278, 279, 280, 281, 282, 283, 284, 285, 286, 287, 288, 289, 290, 291, 300, 301, 302, 303, 304, 305, 306, 307, 316, 317, 318, 319, 320, 321, 322, 323
Node 3 is start node and node 4 is final node.
Those nodes are connected through the following edges:
- 3 to 6 labelled a_1(0)
- 4 to 4 labelled #_1(0)
- 6 to 8 labelled b_1(0)
- 8 to 10 labelled a_1(0)
- 8 to 276 labelled a_1(1)
- 10 to 12 labelled a_1(0)
- 12 to 14 labelled b_1(0)
- 14 to 16 labelled a_1(0)
- 14 to 284 labelled a_1(1)
- 16 to 17 labelled a_1(0)
- 16 to 41 labelled a_1(1)
- 17 to 19 labelled a_1(0)
- 19 to 4 labelled b_1(0)
- 41 to 42 labelled b_1(1)
- 42 to 43 labelled a_1(1)
- 42 to 300 labelled a_1(2)
- 43 to 44 labelled a_1(1)
- 44 to 45 labelled b_1(1)
- 45 to 46 labelled a_1(1)
- 45 to 316 labelled a_1(2)
- 46 to 47 labelled a_1(1)
- 46 to 41 labelled a_1(1)
- 47 to 48 labelled a_1(1)
- 48 to 4 labelled b_1(1)
- 276 to 277 labelled b_1(1)
- 277 to 278 labelled a_1(1)
- 278 to 279 labelled a_1(1)
- 279 to 280 labelled b_1(1)
- 280 to 281 labelled a_1(1)
- 281 to 282 labelled a_1(1)
- 282 to 283 labelled a_1(1)
- 283 to 43 labelled b_1(1)
- 283 to 300 labelled b_1(1)
- 284 to 285 labelled b_1(1)
- 285 to 286 labelled a_1(1)
- 285 to 300 labelled a_1(2)
- 286 to 287 labelled a_1(1)
- 287 to 288 labelled b_1(1)
- 288 to 289 labelled a_1(1)
- 288 to 316 labelled a_1(2)
- 289 to 290 labelled a_1(1)
- 289 to 41 labelled a_1(1)
- 290 to 291 labelled a_1(1)
- 291 to 46 labelled b_1(1)
- 291 to 316 labelled b_1(1)
- 300 to 301 labelled b_1(2)
- 301 to 302 labelled a_1(2)
- 302 to 303 labelled a_1(2)
- 303 to 304 labelled b_1(2)
- 304 to 305 labelled a_1(2)
- 305 to 306 labelled a_1(2)
- 306 to 307 labelled a_1(2)
- 307 to 43 labelled b_1(2)
- 307 to 300 labelled b_1(2)
- 316 to 317 labelled b_1(2)
- 317 to 318 labelled a_1(2)
- 317 to 300 labelled a_1(2)
- 318 to 319 labelled a_1(2)
- 319 to 320 labelled b_1(2)
- 320 to 321 labelled a_1(2)
- 320 to 316 labelled a_1(2)
- 321 to 322 labelled a_1(2)
- 321 to 41 labelled a_1(1)
- 322 to 323 labelled a_1(2)
- 323 to 46 labelled b_1(2)
- 323 to 316 labelled b_1(2)