(1) RFCMatchBoundsTRSProof (EQUIVALENT transformation)
Termination of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 7. This implies Q-termination of R.
The following rules were used to construct the certificate:
active(f(f(a))) → mark(c(f(g(f(a)))))
active(f(X)) → f(active(X))
active(g(X)) → g(active(X))
f(mark(X)) → mark(f(X))
g(mark(X)) → mark(g(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(c(X)) → c(proper(X))
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(X))
c(ok(X)) → ok(c(X))
g(ok(X)) → ok(g(X))
top(mark(X)) → top(proper(X))
top(ok(X)) → top(active(X))
The certificate found is represented by the following graph.
The certificate consists of the following enumerated nodes:
1714820, 1714821, 1714822, 1714825, 1714826, 1714827, 1714823, 1714824, 1714828, 1714829, 1714830, 1714831, 1714832, 1714833, 1714834, 1714835, 1714836, 1714837, 1714838, 1714839, 1714840, 1714841, 1714842, 1714843, 1714844, 1714845, 1714846, 1714847, 1714848, 1714850, 1714851, 1714849, 1714852, 1714853, 1714854, 1714855, 1714856, 1714857, 1714858, 1714859, 1714860, 1714861, 1714862, 1714863, 1714864, 1714865, 1714866, 1714867, 1714868, 1714869, 1714870, 1714871, 1714872, 1714873, 1714874, 1714875, 1714876, 1714877, 1714878, 1714879, 1714880, 1714881
Node 1714820 is start node and node 1714821 is final node.
Those nodes are connect through the following edges:
- 1714820 to 1714822 labelled ok_1(0), mark_1(0)
- 1714820 to 1714823 labelled mark_1(0), ok_1(0)
- 1714820 to 1714828 labelled g_1(0), top_1(0), f_1(0), c_1(0)
- 1714820 to 1714827 labelled ok_1(0)
- 1714820 to 1714838 labelled ok_1(1)
- 1714820 to 1714839 labelled top_1(1)
- 1714820 to 1714840 labelled mark_1(1)
- 1714820 to 1714854 labelled top_1(2)
- 1714820 to 1714876 labelled top_1(3)
- 1714821 to 1714821 labelled #_1(0)
- 1714822 to 1714821 labelled g_1(0), c_1(0)
- 1714822 to 1714829 labelled ok_1(1), mark_1(1)
- 1714825 to 1714826 labelled g_1(0)
- 1714826 to 1714827 labelled f_1(0)
- 1714827 to 1714821 labelled a(0)
- 1714823 to 1714824 labelled c_1(0)
- 1714823 to 1714821 labelled f_1(0)
- 1714823 to 1714830 labelled mark_1(1), ok_1(1)
- 1714824 to 1714825 labelled f_1(0)
- 1714828 to 1714821 labelled proper_1(0), active_1(0)
- 1714828 to 1714831 labelled g_1(1), f_1(1), c_1(1)
- 1714828 to 1714832 labelled ok_1(1)
- 1714828 to 1714833 labelled mark_1(1)
- 1714828 to 1714842 labelled ok_1(2)
- 1714828 to 1714843 labelled mark_1(2)
- 1714829 to 1714821 labelled g_1(1), c_1(1)
- 1714829 to 1714829 labelled ok_1(1), mark_1(1)
- 1714830 to 1714821 labelled f_1(1)
- 1714830 to 1714830 labelled mark_1(1), ok_1(1)
- 1714831 to 1714821 labelled proper_1(1), active_1(1)
- 1714831 to 1714831 labelled g_1(1), f_1(1), c_1(1)
- 1714831 to 1714832 labelled ok_1(1)
- 1714831 to 1714833 labelled mark_1(1)
- 1714831 to 1714842 labelled ok_1(2)
- 1714831 to 1714843 labelled mark_1(2)
- 1714832 to 1714821 labelled a(1)
- 1714833 to 1714834 labelled c_1(1)
- 1714834 to 1714835 labelled f_1(1)
- 1714835 to 1714836 labelled g_1(1)
- 1714836 to 1714837 labelled f_1(1)
- 1714837 to 1714821 labelled a(1)
- 1714838 to 1714832 labelled g_1(1), f_1(1), c_1(1)
- 1714838 to 1714842 labelled g_1(1), f_1(1), c_1(1)
- 1714839 to 1714832 labelled active_1(1)
- 1714839 to 1714833 labelled proper_1(1)
- 1714839 to 1714841 labelled c_1(2)
- 1714839 to 1714843 labelled proper_1(1)
- 1714839 to 1714842 labelled active_1(1)
- 1714839 to 1714845 labelled g_1(2), f_1(2)
- 1714839 to 1714847 labelled mark_1(2)
- 1714839 to 1714856 labelled mark_1(3)
- 1714839 to 1714866 labelled ok_1(3)
- 1714840 to 1714833 labelled g_1(1), f_1(1)
- 1714840 to 1714843 labelled g_1(1), f_1(1)
- 1714841 to 1714834 labelled proper_1(2)
- 1714841 to 1714844 labelled f_1(2)
- 1714841 to 1714864 labelled ok_1(3)
- 1714842 to 1714832 labelled c_1(2), f_1(2), g_1(2)
- 1714842 to 1714842 labelled c_1(2), f_1(2), g_1(2)
- 1714843 to 1714833 labelled f_1(2), g_1(2)
- 1714843 to 1714843 labelled f_1(2), g_1(2)
- 1714844 to 1714835 labelled proper_1(2)
- 1714844 to 1714846 labelled g_1(2)
- 1714844 to 1714862 labelled ok_1(3)
- 1714845 to 1714842 labelled active_1(2)
- 1714845 to 1714843 labelled proper_1(2)
- 1714845 to 1714832 labelled active_1(2)
- 1714845 to 1714833 labelled proper_1(2)
- 1714845 to 1714841 labelled c_1(2)
- 1714845 to 1714852 labelled g_1(3), f_1(3)
- 1714845 to 1714847 labelled mark_1(2)
- 1714845 to 1714856 labelled mark_1(3)
- 1714845 to 1714861 labelled mark_1(4)
- 1714845 to 1714866 labelled ok_1(3)
- 1714845 to 1714870 labelled ok_1(4)
- 1714846 to 1714836 labelled proper_1(2)
- 1714846 to 1714853 labelled f_1(2)
- 1714846 to 1714858 labelled ok_1(3)
- 1714847 to 1714848 labelled c_1(2)
- 1714848 to 1714849 labelled f_1(2)
- 1714850 to 1714851 labelled f_1(2)
- 1714851 to 1714821 labelled a(2)
- 1714849 to 1714850 labelled g_1(2)
- 1714852 to 1714842 labelled active_1(3)
- 1714852 to 1714843 labelled proper_1(3)
- 1714852 to 1714832 labelled active_1(3)
- 1714852 to 1714833 labelled proper_1(3)
- 1714852 to 1714841 labelled c_1(2)
- 1714852 to 1714852 labelled f_1(3), g_1(3)
- 1714852 to 1714847 labelled mark_1(2)
- 1714852 to 1714856 labelled mark_1(3)
- 1714852 to 1714861 labelled mark_1(4)
- 1714852 to 1714866 labelled ok_1(3)
- 1714852 to 1714870 labelled ok_1(4)
- 1714853 to 1714837 labelled proper_1(2)
- 1714853 to 1714851 labelled ok_1(2)
- 1714854 to 1714847 labelled proper_1(2)
- 1714854 to 1714855 labelled c_1(3)
- 1714854 to 1714856 labelled proper_1(2)
- 1714854 to 1714859 labelled g_1(3), f_1(3)
- 1714854 to 1714866 labelled active_1(2)
- 1714854 to 1714874 labelled ok_1(4)
- 1714855 to 1714848 labelled proper_1(3)
- 1714855 to 1714857 labelled f_1(3)
- 1714855 to 1714873 labelled ok_1(4)
- 1714856 to 1714847 labelled g_1(3), f_1(3)
- 1714856 to 1714856 labelled g_1(3), f_1(3)
- 1714856 to 1714861 labelled g_1(3), f_1(3)
- 1714857 to 1714849 labelled proper_1(3)
- 1714857 to 1714860 labelled g_1(3)
- 1714857 to 1714872 labelled ok_1(4)
- 1714858 to 1714851 labelled f_1(3)
- 1714859 to 1714847 labelled proper_1(3)
- 1714859 to 1714855 labelled c_1(3)
- 1714859 to 1714856 labelled proper_1(3)
- 1714859 to 1714865 labelled g_1(4), f_1(4)
- 1714859 to 1714861 labelled proper_1(3)
- 1714859 to 1714866 labelled active_1(3)
- 1714859 to 1714870 labelled active_1(3)
- 1714859 to 1714874 labelled ok_1(4)
- 1714859 to 1714875 labelled ok_1(5)
- 1714860 to 1714850 labelled proper_1(3)
- 1714860 to 1714863 labelled f_1(3)
- 1714860 to 1714868 labelled ok_1(4)
- 1714861 to 1714856 labelled f_1(4), g_1(4)
- 1714861 to 1714861 labelled f_1(4), g_1(4)
- 1714862 to 1714858 labelled g_1(3)
- 1714863 to 1714851 labelled proper_1(3)
- 1714863 to 1714867 labelled ok_1(3)
- 1714864 to 1714862 labelled f_1(3)
- 1714865 to 1714847 labelled proper_1(4)
- 1714865 to 1714856 labelled proper_1(4)
- 1714865 to 1714861 labelled proper_1(4)
- 1714865 to 1714865 labelled g_1(4), f_1(4)
- 1714865 to 1714869 labelled f_1(5), g_1(5)
- 1714865 to 1714855 labelled c_1(3)
- 1714865 to 1714871 labelled g_1(5), f_1(5)
- 1714865 to 1714866 labelled active_1(4)
- 1714865 to 1714870 labelled active_1(4)
- 1714865 to 1714874 labelled ok_1(4)
- 1714865 to 1714875 labelled ok_1(5)
- 1714865 to 1714877 labelled ok_1(6)
- 1714866 to 1714864 labelled c_1(3)
- 1714866 to 1714866 labelled g_1(3), f_1(3)
- 1714866 to 1714870 labelled g_1(3), f_1(3)
- 1714867 to 1714821 labelled a(3)
- 1714868 to 1714867 labelled f_1(4)
- 1714869 to 1714856 labelled proper_1(5)
- 1714869 to 1714865 labelled g_1(4), f_1(4)
- 1714869 to 1714866 labelled active_1(5)
- 1714869 to 1714870 labelled active_1(5)
- 1714869 to 1714875 labelled ok_1(5)
- 1714869 to 1714869 labelled g_1(5), f_1(5)
- 1714869 to 1714877 labelled ok_1(6)
- 1714870 to 1714866 labelled f_1(4), g_1(4)
- 1714870 to 1714870 labelled f_1(4), g_1(4)
- 1714871 to 1714861 labelled proper_1(5)
- 1714871 to 1714869 labelled f_1(5), g_1(5)
- 1714871 to 1714871 labelled g_1(5), f_1(5)
- 1714871 to 1714877 labelled ok_1(6)
- 1714872 to 1714868 labelled g_1(4)
- 1714873 to 1714872 labelled f_1(4)
- 1714874 to 1714873 labelled c_1(4)
- 1714874 to 1714874 labelled g_1(4), f_1(4)
- 1714874 to 1714875 labelled g_1(4), f_1(4)
- 1714875 to 1714874 labelled g_1(5), f_1(5)
- 1714875 to 1714875 labelled g_1(5), f_1(5)
- 1714875 to 1714877 labelled g_1(5), f_1(5)
- 1714876 to 1714874 labelled active_1(3)
- 1714876 to 1714878 labelled g_1(4), f_1(4)
- 1714877 to 1714875 labelled g_1(6), f_1(6)
- 1714877 to 1714877 labelled f_1(6), g_1(6)
- 1714878 to 1714874 labelled active_1(4)
- 1714878 to 1714879 labelled f_1(5), g_1(5)
- 1714878 to 1714875 labelled active_1(4)
- 1714879 to 1714875 labelled active_1(5)
- 1714879 to 1714874 labelled active_1(5)
- 1714879 to 1714879 labelled f_1(5), g_1(5)
- 1714879 to 1714880 labelled f_1(6), g_1(6)
- 1714879 to 1714877 labelled active_1(5)
- 1714880 to 1714874 labelled active_1(6)
- 1714880 to 1714877 labelled active_1(6)
- 1714880 to 1714875 labelled active_1(6)
- 1714880 to 1714879 labelled f_1(5), g_1(5)
- 1714880 to 1714880 labelled f_1(6), g_1(6)
- 1714880 to 1714881 labelled f_1(7), g_1(7)
- 1714881 to 1714875 labelled active_1(7)
- 1714881 to 1714877 labelled active_1(7)
- 1714881 to 1714880 labelled f_1(6), g_1(6)
- 1714881 to 1714881 labelled f_1(7), g_1(7)