(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:
f(0) → s(0)
f(s(0)) → s(0)
f(s(s(x))) → f(f(s(x)))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
7541150, 7541151, 7541152, 7541153, 7541154, 7541155, 7541156, 7541157, 7541158
Node 7541150 is start node and node 7541151 is final node.
Those nodes are connect through the following edges:
- 7541150 to 7541152 labelled s_1(0)
- 7541150 to 7541153 labelled f_1(0)
- 7541150 to 7541157 labelled s_1(1)
- 7541151 to 7541151 labelled #_1(0)
- 7541152 to 7541151 labelled 0(0)
- 7541153 to 7541154 labelled f_1(0)
- 7541153 to 7541155 labelled f_1(1)
- 7541153 to 7541157 labelled s_1(1)
- 7541153 to 7541158 labelled s_1(2)
- 7541154 to 7541151 labelled s_1(0)
- 7541155 to 7541156 labelled f_1(1)
- 7541155 to 7541155 labelled f_1(1)
- 7541155 to 7541157 labelled s_1(1)
- 7541155 to 7541158 labelled s_1(2)
- 7541156 to 7541151 labelled s_1(1)
- 7541157 to 7541151 labelled 0(1)
- 7541158 to 7541151 labelled 0(2)