(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(b(a(a(x)))) → a(a(a(a(a(b(b(b(x))))))))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
3, 4, 5, 6, 7, 8, 9, 10, 11, 24, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 68, 69, 70, 71, 72, 73, 74, 89, 90, 91, 92, 93, 94, 95, 103, 104, 105, 106, 107, 108, 109, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127, 128, 129, 130, 152, 153, 154, 155, 156, 157, 158
Node 3 is start node and node 4 is final node.
Those nodes are connected through the following edges:
- 3 to 5 labelled a_1(0)
- 4 to 4 labelled #_1(0)
- 5 to 6 labelled a_1(0)
- 6 to 7 labelled a_1(0)
- 7 to 8 labelled a_1(0)
- 8 to 9 labelled a_1(0)
- 9 to 10 labelled b_1(0)
- 9 to 33 labelled a_1(1)
- 10 to 11 labelled b_1(0)
- 10 to 24 labelled a_1(1)
- 11 to 4 labelled b_1(0)
- 11 to 24 labelled a_1(1)
- 24 to 27 labelled a_1(1)
- 27 to 28 labelled a_1(1)
- 28 to 29 labelled a_1(1)
- 29 to 30 labelled a_1(1)
- 30 to 31 labelled b_1(1)
- 30 to 40 labelled a_1(2)
- 31 to 32 labelled b_1(1)
- 31 to 24 labelled a_1(1)
- 32 to 4 labelled b_1(1)
- 32 to 24 labelled a_1(1)
- 33 to 34 labelled a_1(1)
- 34 to 35 labelled a_1(1)
- 35 to 36 labelled a_1(1)
- 36 to 37 labelled a_1(1)
- 37 to 38 labelled b_1(1)
- 38 to 39 labelled b_1(1)
- 38 to 47 labelled a_1(2)
- 39 to 27 labelled b_1(1)
- 40 to 41 labelled a_1(2)
- 41 to 42 labelled a_1(2)
- 42 to 43 labelled a_1(2)
- 43 to 44 labelled a_1(2)
- 44 to 45 labelled b_1(2)
- 45 to 46 labelled b_1(2)
- 45 to 47 labelled a_1(2)
- 46 to 27 labelled b_1(2)
- 47 to 48 labelled a_1(2)
- 48 to 49 labelled a_1(2)
- 49 to 50 labelled a_1(2)
- 50 to 51 labelled a_1(2)
- 51 to 52 labelled b_1(2)
- 52 to 53 labelled b_1(2)
- 52 to 54 labelled a_1(2)
- 53 to 29 labelled b_1(2)
- 54 to 55 labelled a_1(2)
- 55 to 56 labelled a_1(2)
- 56 to 57 labelled a_1(2)
- 57 to 58 labelled a_1(2)
- 58 to 59 labelled b_1(2)
- 59 to 60 labelled b_1(2)
- 59 to 68 labelled a_1(3)
- 60 to 40 labelled b_1(2)
- 68 to 69 labelled a_1(3)
- 69 to 70 labelled a_1(3)
- 70 to 71 labelled a_1(3)
- 71 to 72 labelled a_1(3)
- 72 to 73 labelled b_1(3)
- 73 to 74 labelled b_1(3)
- 73 to 89 labelled a_1(3)
- 74 to 42 labelled b_1(3)
- 89 to 90 labelled a_1(3)
- 90 to 91 labelled a_1(3)
- 91 to 92 labelled a_1(3)
- 92 to 93 labelled a_1(3)
- 93 to 94 labelled b_1(3)
- 93 to 117 labelled a_1(4)
- 94 to 95 labelled b_1(3)
- 95 to 44 labelled b_1(3)
- 95 to 103 labelled a_1(3)
- 103 to 104 labelled a_1(3)
- 104 to 105 labelled a_1(3)
- 105 to 106 labelled a_1(3)
- 106 to 107 labelled a_1(3)
- 107 to 108 labelled b_1(3)
- 108 to 109 labelled b_1(3)
- 108 to 124 labelled a_1(3)
- 109 to 48 labelled b_1(3)
- 117 to 118 labelled a_1(4)
- 118 to 119 labelled a_1(4)
- 119 to 120 labelled a_1(4)
- 120 to 121 labelled a_1(4)
- 121 to 122 labelled b_1(4)
- 122 to 123 labelled b_1(4)
- 122 to 152 labelled a_1(4)
- 123 to 104 labelled b_1(4)
- 124 to 125 labelled a_1(3)
- 125 to 126 labelled a_1(3)
- 126 to 127 labelled a_1(3)
- 127 to 128 labelled a_1(3)
- 128 to 129 labelled b_1(3)
- 129 to 130 labelled b_1(3)
- 130 to 50 labelled b_1(3)
- 152 to 153 labelled a_1(4)
- 153 to 154 labelled a_1(4)
- 154 to 155 labelled a_1(4)
- 155 to 156 labelled a_1(4)
- 156 to 157 labelled b_1(4)
- 157 to 158 labelled b_1(4)
- 158 to 106 labelled b_1(4)