(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 3. This implies Q-termination of R.
The following rules were used to construct the certificate:
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(X))
mark(a) → active(a)
mark(g(X)) → active(g(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
1692200, 1692201, 1692204, 1692205, 1692203, 1692202, 1692206, 1692207, 1692208, 1692209, 1692210, 1692211, 1692212, 1692213, 1692214, 1692215
Node 1692200 is start node and node 1692201 is final node.
Those nodes are connect through the following edges:
- 1692200 to 1692201 labelled g_1(0), f_1(0), g_1(1), f_1(1)
- 1692200 to 1692202 labelled mark_1(0)
- 1692200 to 1692206 labelled active_1(0)
- 1692200 to 1692200 labelled active_1(0)
- 1692200 to 1692205 labelled active_1(0)
- 1692200 to 1692210 labelled active_1(1)
- 1692200 to 1692211 labelled mark_1(1)
- 1692200 to 1692215 labelled active_1(2)
- 1692201 to 1692201 labelled #_1(0)
- 1692204 to 1692205 labelled f_1(0)
- 1692205 to 1692201 labelled a(0)
- 1692203 to 1692204 labelled g_1(0)
- 1692202 to 1692203 labelled f_1(0)
- 1692206 to 1692207 labelled g_1(0)
- 1692206 to 1692201 labelled g_1(1)
- 1692206 to 1692208 labelled g_1(1)
- 1692206 to 1692211 labelled g_1(1)
- 1692206 to 1692215 labelled g_1(1)
- 1692207 to 1692201 labelled mark_1(0)
- 1692207 to 1692208 labelled active_1(1)
- 1692207 to 1692211 labelled mark_1(1)
- 1692207 to 1692215 labelled active_1(2)
- 1692208 to 1692209 labelled g_1(1)
- 1692208 to 1692201 labelled f_1(1), a(1), g_1(2), g_1(1)
- 1692208 to 1692200 labelled g_1(2), g_1(1)
- 1692208 to 1692208 labelled g_1(2)
- 1692208 to 1692211 labelled g_1(2)
- 1692208 to 1692206 labelled g_1(1)
- 1692208 to 1692205 labelled g_1(1)
- 1692208 to 1692210 labelled g_1(2)
- 1692208 to 1692202 labelled g_1(1)
- 1692208 to 1692215 labelled g_1(3), g_1(2)
- 1692209 to 1692201 labelled mark_1(1)
- 1692209 to 1692208 labelled active_1(1)
- 1692209 to 1692200 labelled active_1(1)
- 1692209 to 1692211 labelled mark_1(1)
- 1692209 to 1692215 labelled active_1(2)
- 1692210 to 1692203 labelled f_1(1)
- 1692211 to 1692212 labelled f_1(1)
- 1692212 to 1692213 labelled g_1(1)
- 1692213 to 1692214 labelled f_1(1)
- 1692214 to 1692201 labelled a(1)
- 1692215 to 1692212 labelled f_1(2)