(1) 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:
active(f(f(a))) → mark(f(g(f(a))))
mark(f(X)) → active(f(mark(X)))
mark(a) → active(a)
mark(g(X)) → active(g(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:
71871, 71872, 71873, 71874, 71876, 71875, 71877, 71878, 71879, 71880, 71881, 71883, 71884, 71882, 71885, 71886, 71887, 71888, 71889, 71893, 71892, 71890, 71891, 71895, 71894, 71896
Node 71871 is start node and node 71872 is final node.
Those nodes are connect through the following edges:
- 71871 to 71872 labelled g_1(0), f_1(0), f_1(1), g_1(1)
- 71871 to 71873 labelled mark_1(0)
- 71871 to 71871 labelled active_1(0)
- 71871 to 71876 labelled active_1(0)
- 71871 to 71877 labelled active_1(1)
- 71871 to 71882 labelled mark_1(1), g_1(1), f_1(2), f_1(1), g_1(2)
- 71871 to 71879 labelled f_1(1), f_1(2), g_1(2), g_1(1)
- 71871 to 71880 labelled f_1(1), f_1(2), g_1(2), g_1(1)
- 71871 to 71886 labelled active_1(2), g_1(1), f_1(2), f_1(1), g_1(2)
- 71871 to 71890 labelled g_1(1), f_1(2), f_1(1), g_1(2)
- 71871 to 71894 labelled g_1(1), f_1(2), f_1(1), g_1(2)
- 71872 to 71872 labelled #_1(0), mark_1(0)
- 71872 to 71879 labelled active_1(1)
- 71872 to 71880 labelled active_1(1)
- 71872 to 71882 labelled mark_1(1)
- 71872 to 71886 labelled active_1(2)
- 71872 to 71890 labelled mark_1(2)
- 71872 to 71894 labelled active_1(3)
- 71873 to 71874 labelled f_1(0)
- 71874 to 71875 labelled g_1(0)
- 71876 to 71872 labelled a(0)
- 71875 to 71876 labelled f_1(0)
- 71877 to 71878 labelled f_1(1)
- 71877 to 71874 labelled f_1(2)
- 71877 to 71888 labelled f_1(2)
- 71878 to 71874 labelled mark_1(1)
- 71878 to 71888 labelled active_1(1)
- 71879 to 71872 labelled g_1(1), a(1)
- 71879 to 71879 labelled g_1(2)
- 71879 to 71880 labelled g_1(2)
- 71879 to 71882 labelled g_1(2)
- 71879 to 71886 labelled g_1(2)
- 71879 to 71890 labelled g_1(2)
- 71879 to 71894 labelled g_1(2)
- 71880 to 71881 labelled f_1(1)
- 71880 to 71872 labelled f_1(2), f_1(1)
- 71880 to 71880 labelled f_1(2)
- 71880 to 71879 labelled f_1(2)
- 71880 to 71871 labelled f_1(2), f_1(1)
- 71880 to 71882 labelled f_1(2)
- 71880 to 71886 labelled f_1(3), f_1(2)
- 71880 to 71877 labelled f_1(2)
- 71880 to 71873 labelled f_1(1)
- 71880 to 71876 labelled f_1(1)
- 71880 to 71890 labelled f_1(2), f_1(3)
- 71880 to 71894 labelled f_1(2), f_1(3)
- 71881 to 71872 labelled mark_1(1)
- 71881 to 71871 labelled active_1(1)
- 71881 to 71880 labelled active_1(1)
- 71881 to 71879 labelled active_1(1)
- 71881 to 71882 labelled mark_1(1)
- 71881 to 71886 labelled active_1(2)
- 71881 to 71890 labelled mark_1(2)
- 71881 to 71894 labelled active_1(3)
- 71883 to 71884 labelled g_1(1)
- 71884 to 71885 labelled f_1(1)
- 71882 to 71883 labelled f_1(1)
- 71885 to 71872 labelled a(1)
- 71886 to 71887 labelled f_1(2)
- 71886 to 71883 labelled f_1(3)
- 71886 to 71889 labelled f_1(3)
- 71887 to 71883 labelled mark_1(2)
- 71887 to 71889 labelled active_1(2)
- 71888 to 71875 labelled g_1(1)
- 71889 to 71884 labelled g_1(2)
- 71893 to 71872 labelled a(2)
- 71892 to 71893 labelled f_1(2)
- 71890 to 71891 labelled f_1(2)
- 71891 to 71892 labelled g_1(2)
- 71895 to 71891 labelled mark_1(3)
- 71895 to 71896 labelled active_1(3)
- 71894 to 71895 labelled f_1(3)
- 71894 to 71891 labelled f_1(4)
- 71894 to 71896 labelled f_1(4)
- 71896 to 71892 labelled g_1(3)