(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(X)) → mark(g(h(f(X))))
mark(f(X)) → active(f(mark(X)))
mark(g(X)) → active(g(X))
mark(h(X)) → active(h(mark(X)))
f(mark(X)) → f(X)
f(active(X)) → f(X)
g(mark(X)) → g(X)
g(active(X)) → g(X)
h(mark(X)) → h(X)
h(active(X)) → h(X)
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
2, 3, 12, 13, 14, 15, 16, 17, 18, 19, 23, 24, 25, 30, 31, 32, 33, 34, 35, 36, 37, 42
Node 2 is start node and node 3 is final node.
Those nodes are connected through the following edges:
- 2 to 12 labelled mark_1(0)
- 2 to 15 labelled active_1(0)
- 2 to 17 labelled active_1(0)
- 2 to 3 labelled f_1(0), g_1(0), h_1(0), f_1(1), g_1(1), h_1(1)
- 2 to 19 labelled active_1(1)
- 2 to 23 labelled mark_1(1)
- 2 to 37 labelled active_1(2)
- 3 to 3 labelled #_1(0)
- 12 to 13 labelled g_1(0)
- 13 to 14 labelled h_1(0)
- 14 to 3 labelled f_1(0), f_1(1)
- 15 to 16 labelled f_1(0)
- 15 to 3 labelled g_1(0), g_1(1), f_1(1)
- 15 to 30 labelled f_1(1)
- 15 to 15 labelled f_1(1)
- 15 to 32 labelled f_1(1)
- 15 to 23 labelled f_1(1)
- 15 to 34 labelled f_1(1)
- 15 to 37 labelled f_1(1)
- 15 to 42 labelled f_1(1)
- 16 to 3 labelled mark_1(0)
- 16 to 30 labelled active_1(1)
- 16 to 15 labelled active_1(1)
- 16 to 32 labelled active_1(1)
- 16 to 23 labelled mark_1(1)
- 16 to 34 labelled mark_1(2)
- 16 to 37 labelled active_1(2)
- 16 to 42 labelled active_1(3)
- 17 to 18 labelled h_1(0)
- 17 to 3 labelled h_1(1)
- 17 to 30 labelled h_1(1)
- 17 to 15 labelled h_1(1)
- 17 to 32 labelled h_1(1)
- 17 to 23 labelled h_1(1)
- 17 to 34 labelled h_1(1)
- 17 to 37 labelled h_1(1)
- 17 to 42 labelled h_1(1)
- 18 to 3 labelled mark_1(0)
- 18 to 30 labelled active_1(1)
- 18 to 15 labelled active_1(1)
- 18 to 32 labelled active_1(1)
- 18 to 23 labelled mark_1(1)
- 18 to 34 labelled mark_1(2)
- 18 to 37 labelled active_1(2)
- 18 to 42 labelled active_1(3)
- 19 to 13 labelled g_1(1)
- 23 to 24 labelled g_1(1)
- 24 to 25 labelled h_1(1)
- 25 to 16 labelled f_1(1)
- 25 to 3 labelled f_1(1)
- 25 to 30 labelled f_1(2), f_1(1)
- 25 to 15 labelled f_1(2), f_1(1)
- 25 to 32 labelled f_1(2), f_1(1)
- 25 to 23 labelled f_1(2), f_1(1)
- 25 to 34 labelled f_1(2), f_1(1)
- 25 to 37 labelled f_1(2), f_1(1)
- 25 to 42 labelled f_1(2), f_1(1)
- 30 to 31 labelled f_1(1)
- 30 to 3 labelled f_1(2), f_1(1)
- 30 to 30 labelled f_1(2)
- 30 to 15 labelled f_1(2)
- 30 to 32 labelled f_1(2)
- 30 to 23 labelled f_1(2)
- 30 to 34 labelled f_1(2)
- 30 to 37 labelled f_1(2)
- 30 to 42 labelled f_1(2)
- 31 to 3 labelled mark_1(1)
- 31 to 30 labelled active_1(1)
- 31 to 15 labelled active_1(1)
- 31 to 32 labelled active_1(1)
- 31 to 23 labelled mark_1(1)
- 31 to 34 labelled mark_1(2)
- 31 to 37 labelled active_1(2)
- 31 to 42 labelled active_1(3)
- 32 to 33 labelled h_1(1)
- 32 to 3 labelled h_1(2), h_1(1)
- 32 to 30 labelled h_1(2)
- 32 to 15 labelled h_1(2)
- 32 to 32 labelled h_1(2)
- 32 to 23 labelled h_1(2)
- 32 to 34 labelled h_1(2)
- 32 to 37 labelled h_1(2)
- 32 to 42 labelled h_1(2)
- 33 to 3 labelled mark_1(1)
- 33 to 30 labelled active_1(1)
- 33 to 15 labelled active_1(1)
- 33 to 32 labelled active_1(1)
- 33 to 23 labelled mark_1(1)
- 33 to 34 labelled mark_1(2)
- 33 to 37 labelled active_1(2)
- 33 to 42 labelled active_1(3)
- 34 to 35 labelled g_1(2)
- 35 to 36 labelled h_1(2)
- 36 to 3 labelled f_1(2), f_1(1)
- 36 to 31 labelled f_1(2)
- 36 to 30 labelled f_1(2)
- 36 to 15 labelled f_1(2)
- 36 to 32 labelled f_1(2)
- 36 to 23 labelled f_1(2)
- 36 to 34 labelled f_1(2), f_1(3)
- 36 to 37 labelled f_1(2), f_1(3)
- 36 to 42 labelled f_1(2), f_1(3)
- 37 to 24 labelled g_1(2)
- 42 to 35 labelled g_1(3)