(1) 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:
s1(s1(s0(s0(x)))) → s0(s0(s0(s1(s1(s1(x))))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
9165385, 9165386, 9165388, 9165389, 9165390, 9165391, 9165387, 9165393, 9165394, 9165395, 9165392, 9165396, 9165401, 9165399, 9165400, 9165397, 9165398, 9165402, 9165403, 9165405, 9165406, 9165404, 9165410, 9165411, 9165409, 9165407, 9165408, 9165416, 9165413, 9165414, 9165415, 9165412, 9165420, 9165421, 9165417, 9165418, 9165419, 9165423, 9165424, 9165425, 9165426, 9165422
Node 9165385 is start node and node 9165386 is final node.
Those nodes are connect through the following edges:
- 9165385 to 9165387 labelled s0_1(0)
- 9165386 to 9165386 labelled #_1(0)
- 9165388 to 9165389 labelled s0_1(0)
- 9165389 to 9165390 labelled s1_1(0)
- 9165389 to 9165397 labelled s0_1(1)
- 9165390 to 9165391 labelled s1_1(0)
- 9165390 to 9165392 labelled s0_1(1)
- 9165391 to 9165386 labelled s1_1(0)
- 9165391 to 9165392 labelled s0_1(1)
- 9165387 to 9165388 labelled s0_1(0)
- 9165393 to 9165394 labelled s0_1(1)
- 9165394 to 9165395 labelled s1_1(1)
- 9165394 to 9165402 labelled s0_1(2)
- 9165395 to 9165396 labelled s1_1(1)
- 9165395 to 9165392 labelled s0_1(1)
- 9165392 to 9165393 labelled s0_1(1)
- 9165396 to 9165386 labelled s1_1(1)
- 9165396 to 9165392 labelled s0_1(1)
- 9165401 to 9165393 labelled s1_1(1)
- 9165399 to 9165400 labelled s1_1(1)
- 9165400 to 9165401 labelled s1_1(1)
- 9165400 to 9165407 labelled s0_1(2)
- 9165397 to 9165398 labelled s0_1(1)
- 9165398 to 9165399 labelled s0_1(1)
- 9165402 to 9165403 labelled s0_1(2)
- 9165403 to 9165404 labelled s0_1(2)
- 9165405 to 9165406 labelled s1_1(2)
- 9165405 to 9165407 labelled s0_1(2)
- 9165406 to 9165393 labelled s1_1(2)
- 9165404 to 9165405 labelled s1_1(2)
- 9165410 to 9165411 labelled s1_1(2)
- 9165410 to 9165412 labelled s0_1(3)
- 9165411 to 9165402 labelled s1_1(2)
- 9165409 to 9165410 labelled s1_1(2)
- 9165407 to 9165408 labelled s0_1(2)
- 9165408 to 9165409 labelled s0_1(2)
- 9165416 to 9165404 labelled s1_1(3)
- 9165416 to 9165417 labelled s0_1(3)
- 9165413 to 9165414 labelled s0_1(3)
- 9165414 to 9165415 labelled s1_1(3)
- 9165414 to 9165422 labelled s0_1(4)
- 9165415 to 9165416 labelled s1_1(3)
- 9165412 to 9165413 labelled s0_1(3)
- 9165420 to 9165421 labelled s1_1(3)
- 9165421 to 9165408 labelled s1_1(3)
- 9165417 to 9165418 labelled s0_1(3)
- 9165418 to 9165419 labelled s0_1(3)
- 9165419 to 9165420 labelled s1_1(3)
- 9165423 to 9165424 labelled s0_1(4)
- 9165424 to 9165425 labelled s1_1(4)
- 9165425 to 9165426 labelled s1_1(4)
- 9165426 to 9165418 labelled s1_1(4)
- 9165422 to 9165423 labelled s0_1(4)