(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:
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:
2, 4, 5, 8, 9, 11, 13, 15, 16, 19, 23, 24, 25, 26, 27, 28, 33
Node 2 is start node and node 4 is final node.
Those nodes are connected through the following edges:
- 2 to 5 labelled mark_1(0)
- 2 to 13 labelled active_1(0)
- 2 to 11 labelled active_1(0)
- 2 to 15 labelled active_1(0)
- 2 to 4 labelled f_1(0), g_1(0), f_1(1), g_1(1)
- 2 to 19 labelled active_1(1)
- 2 to 25 labelled mark_1(1)
- 2 to 33 labelled active_1(2)
- 4 to 4 labelled #_1(0)
- 5 to 8 labelled f_1(0)
- 8 to 9 labelled g_1(0)
- 9 to 11 labelled f_1(0)
- 11 to 4 labelled a(0)
- 13 to 4 labelled f_1(0), f_1(1), a(1)
- 15 to 16 labelled g_1(0)
- 15 to 4 labelled g_1(1)
- 15 to 13 labelled g_1(1)
- 15 to 23 labelled g_1(1)
- 15 to 25 labelled g_1(1)
- 15 to 33 labelled g_1(1)
- 16 to 4 labelled mark_1(0)
- 16 to 13 labelled active_1(1)
- 16 to 23 labelled active_1(1)
- 16 to 25 labelled mark_1(1)
- 16 to 33 labelled active_1(2)
- 19 to 8 labelled f_1(1)
- 23 to 24 labelled g_1(1)
- 23 to 4 labelled g_1(2), g_1(1)
- 23 to 13 labelled g_1(2)
- 23 to 23 labelled g_1(2)
- 23 to 25 labelled g_1(2)
- 23 to 33 labelled g_1(2)
- 24 to 4 labelled mark_1(1)
- 24 to 13 labelled active_1(1)
- 24 to 23 labelled active_1(1)
- 24 to 25 labelled mark_1(1)
- 24 to 33 labelled active_1(2)
- 25 to 26 labelled f_1(1)
- 26 to 27 labelled g_1(1)
- 27 to 28 labelled f_1(1)
- 28 to 4 labelled a(1)
- 33 to 26 labelled f_1(2)