(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:
10095862, 10095863, 10095864, 10095869, 10095865, 10095868, 10095866, 10095867, 10095870, 10095871, 10095872, 10095873, 10095877, 10095878, 10095875, 10095876, 10095874, 10095879, 10095880, 10095881, 10095882, 10095883, 10095884, 10095885, 10095886, 10095887, 10095888, 10095889, 10095894, 10095892, 10095893, 10095891, 10095890, 10095895, 10095896, 10095897, 10095898, 10095899, 10095900, 10095901, 10095902, 10095903, 10095904, 10095905, 10095906, 10095907, 10095908, 10095909, 10095910, 10095911, 10095912, 10095913, 10095914, 10095915, 10095916, 10095917, 10095918, 10095919, 10095920, 10095921, 10095922, 10095923, 10095924, 10095925, 10095926
Node 10095862 is start node and node 10095863 is final node.
Those nodes are connect through the following edges:
- 10095862 to 10095864 labelled ok_1(0), mark_1(0)
- 10095862 to 10095865 labelled mark_1(0), ok_1(0)
- 10095862 to 10095870 labelled g_1(0), top_1(0), f_1(0), c_1(0)
- 10095862 to 10095869 labelled ok_1(0)
- 10095862 to 10095880 labelled ok_1(1)
- 10095862 to 10095881 labelled top_1(1)
- 10095862 to 10095882 labelled mark_1(1)
- 10095862 to 10095899 labelled top_1(2)
- 10095862 to 10095920 labelled top_1(3)
- 10095863 to 10095863 labelled #_1(0)
- 10095864 to 10095863 labelled g_1(0), c_1(0)
- 10095864 to 10095879 labelled ok_1(1), mark_1(1)
- 10095869 to 10095863 labelled a(0)
- 10095865 to 10095866 labelled c_1(0)
- 10095865 to 10095863 labelled f_1(0)
- 10095865 to 10095871 labelled mark_1(1), ok_1(1)
- 10095868 to 10095869 labelled f_1(0)
- 10095866 to 10095867 labelled f_1(0)
- 10095867 to 10095868 labelled g_1(0)
- 10095870 to 10095863 labelled proper_1(0), active_1(0)
- 10095870 to 10095872 labelled g_1(1), f_1(1), c_1(1)
- 10095870 to 10095873 labelled ok_1(1)
- 10095870 to 10095874 labelled mark_1(1)
- 10095870 to 10095883 labelled mark_1(2)
- 10095870 to 10095884 labelled ok_1(2)
- 10095871 to 10095863 labelled f_1(1)
- 10095871 to 10095871 labelled mark_1(1), ok_1(1)
- 10095872 to 10095863 labelled proper_1(1), active_1(1)
- 10095872 to 10095872 labelled g_1(1), f_1(1), c_1(1)
- 10095872 to 10095873 labelled ok_1(1)
- 10095872 to 10095874 labelled mark_1(1)
- 10095872 to 10095883 labelled mark_1(2)
- 10095872 to 10095884 labelled ok_1(2)
- 10095873 to 10095863 labelled a(1)
- 10095877 to 10095878 labelled f_1(1)
- 10095878 to 10095863 labelled a(1)
- 10095875 to 10095876 labelled f_1(1)
- 10095876 to 10095877 labelled g_1(1)
- 10095874 to 10095875 labelled c_1(1)
- 10095879 to 10095863 labelled g_1(1), c_1(1)
- 10095879 to 10095879 labelled ok_1(1), mark_1(1)
- 10095880 to 10095873 labelled c_1(1), f_1(1), g_1(1)
- 10095880 to 10095884 labelled c_1(1), f_1(1), g_1(1)
- 10095881 to 10095873 labelled active_1(1)
- 10095881 to 10095874 labelled proper_1(1)
- 10095881 to 10095885 labelled c_1(2)
- 10095881 to 10095883 labelled proper_1(1)
- 10095881 to 10095884 labelled active_1(1)
- 10095881 to 10095887 labelled f_1(2), g_1(2)
- 10095881 to 10095888 labelled g_1(2), f_1(2)
- 10095881 to 10095890 labelled mark_1(2)
- 10095881 to 10095901 labelled mark_1(3)
- 10095881 to 10095911 labelled ok_1(3)
- 10095882 to 10095874 labelled f_1(1), g_1(1)
- 10095882 to 10095883 labelled f_1(1), g_1(1)
- 10095883 to 10095874 labelled g_1(2), f_1(2)
- 10095883 to 10095883 labelled g_1(2), f_1(2)
- 10095884 to 10095873 labelled c_1(2), g_1(2), f_1(2)
- 10095884 to 10095884 labelled c_1(2), g_1(2), f_1(2)
- 10095885 to 10095875 labelled proper_1(2)
- 10095885 to 10095886 labelled f_1(2)
- 10095885 to 10095909 labelled ok_1(3)
- 10095886 to 10095876 labelled proper_1(2)
- 10095886 to 10095889 labelled g_1(2)
- 10095886 to 10095904 labelled ok_1(3)
- 10095887 to 10095874 labelled proper_1(2)
- 10095887 to 10095884 labelled active_1(2)
- 10095887 to 10095873 labelled active_1(2)
- 10095887 to 10095885 labelled c_1(2)
- 10095887 to 10095897 labelled f_1(3), g_1(3)
- 10095887 to 10095890 labelled mark_1(2)
- 10095887 to 10095901 labelled mark_1(3)
- 10095887 to 10095905 labelled mark_1(4)
- 10095887 to 10095911 labelled ok_1(3)
- 10095888 to 10095883 labelled proper_1(2)
- 10095888 to 10095895 labelled f_1(3), g_1(3)
- 10095888 to 10095896 labelled g_1(3), f_1(3)
- 10095888 to 10095915 labelled ok_1(4)
- 10095889 to 10095877 labelled proper_1(2)
- 10095889 to 10095898 labelled f_1(2)
- 10095889 to 10095902 labelled ok_1(3)
- 10095894 to 10095863 labelled a(2)
- 10095892 to 10095893 labelled g_1(2)
- 10095893 to 10095894 labelled f_1(2)
- 10095891 to 10095892 labelled f_1(2)
- 10095890 to 10095891 labelled c_1(2)
- 10095895 to 10095874 labelled proper_1(3)
- 10095895 to 10095885 labelled c_1(2)
- 10095895 to 10095911 labelled ok_1(3)
- 10095896 to 10095883 labelled proper_1(3)
- 10095896 to 10095895 labelled f_1(3), g_1(3)
- 10095896 to 10095896 labelled g_1(3), f_1(3)
- 10095896 to 10095915 labelled ok_1(4)
- 10095897 to 10095884 labelled active_1(3)
- 10095897 to 10095873 labelled active_1(3)
- 10095897 to 10095897 labelled g_1(3), f_1(3)
- 10095897 to 10095890 labelled mark_1(2)
- 10095897 to 10095901 labelled mark_1(3)
- 10095897 to 10095905 labelled mark_1(4)
- 10095898 to 10095878 labelled proper_1(2)
- 10095898 to 10095894 labelled ok_1(2)
- 10095899 to 10095890 labelled proper_1(2)
- 10095899 to 10095900 labelled c_1(3)
- 10095899 to 10095901 labelled proper_1(2)
- 10095899 to 10095906 labelled f_1(3), g_1(3)
- 10095899 to 10095911 labelled active_1(2)
- 10095899 to 10095919 labelled ok_1(4)
- 10095900 to 10095891 labelled proper_1(3)
- 10095900 to 10095903 labelled f_1(3)
- 10095900 to 10095918 labelled ok_1(4)
- 10095901 to 10095890 labelled g_1(3), f_1(3)
- 10095901 to 10095901 labelled g_1(3), f_1(3)
- 10095901 to 10095905 labelled g_1(3), f_1(3)
- 10095902 to 10095894 labelled f_1(3)
- 10095903 to 10095892 labelled proper_1(3)
- 10095903 to 10095907 labelled g_1(3)
- 10095903 to 10095917 labelled ok_1(4)
- 10095904 to 10095902 labelled g_1(3)
- 10095905 to 10095901 labelled g_1(4), f_1(4)
- 10095905 to 10095905 labelled g_1(4), f_1(4)
- 10095906 to 10095890 labelled proper_1(3)
- 10095906 to 10095901 labelled proper_1(3)
- 10095906 to 10095900 labelled c_1(3)
- 10095906 to 10095910 labelled g_1(4), f_1(4)
- 10095906 to 10095905 labelled proper_1(3)
- 10095906 to 10095911 labelled active_1(3)
- 10095906 to 10095915 labelled active_1(3)
- 10095906 to 10095919 labelled ok_1(4)
- 10095906 to 10095921 labelled ok_1(5)
- 10095907 to 10095893 labelled proper_1(3)
- 10095907 to 10095908 labelled f_1(3)
- 10095907 to 10095916 labelled ok_1(4)
- 10095908 to 10095894 labelled proper_1(3)
- 10095908 to 10095912 labelled ok_1(3)
- 10095909 to 10095904 labelled f_1(3)
- 10095910 to 10095901 labelled proper_1(4)
- 10095910 to 10095905 labelled proper_1(4)
- 10095910 to 10095890 labelled proper_1(4)
- 10095910 to 10095913 labelled f_1(5), g_1(5)
- 10095910 to 10095914 labelled g_1(5), f_1(5)
- 10095910 to 10095910 labelled g_1(4), f_1(4)
- 10095910 to 10095900 labelled c_1(3)
- 10095910 to 10095915 labelled active_1(4)
- 10095910 to 10095911 labelled active_1(4)
- 10095910 to 10095919 labelled ok_1(4)
- 10095910 to 10095921 labelled ok_1(5)
- 10095910 to 10095923 labelled ok_1(6)
- 10095911 to 10095909 labelled c_1(3)
- 10095911 to 10095911 labelled g_1(3), f_1(3)
- 10095911 to 10095915 labelled g_1(3), f_1(3)
- 10095912 to 10095863 labelled a(3)
- 10095913 to 10095901 labelled proper_1(5)
- 10095913 to 10095910 labelled g_1(4), f_1(4)
- 10095913 to 10095911 labelled active_1(5)
- 10095913 to 10095915 labelled active_1(5)
- 10095913 to 10095913 labelled f_1(5), g_1(5)
- 10095913 to 10095921 labelled ok_1(5)
- 10095913 to 10095923 labelled ok_1(6)
- 10095914 to 10095905 labelled proper_1(5)
- 10095914 to 10095913 labelled f_1(5), g_1(5)
- 10095914 to 10095914 labelled g_1(5), f_1(5)
- 10095914 to 10095923 labelled ok_1(6)
- 10095915 to 10095911 labelled g_1(4), f_1(4)
- 10095915 to 10095915 labelled f_1(4), g_1(4)
- 10095916 to 10095912 labelled f_1(4)
- 10095917 to 10095916 labelled g_1(4)
- 10095918 to 10095917 labelled f_1(4)
- 10095919 to 10095918 labelled c_1(4)
- 10095919 to 10095919 labelled g_1(4), f_1(4)
- 10095919 to 10095921 labelled g_1(4), f_1(4)
- 10095920 to 10095919 labelled active_1(3)
- 10095920 to 10095922 labelled g_1(4), f_1(4)
- 10095921 to 10095919 labelled f_1(5), g_1(5)
- 10095921 to 10095921 labelled f_1(5), g_1(5)
- 10095921 to 10095923 labelled f_1(5), g_1(5)
- 10095922 to 10095919 labelled active_1(4)
- 10095922 to 10095924 labelled g_1(5), f_1(5)
- 10095922 to 10095921 labelled active_1(4)
- 10095923 to 10095921 labelled g_1(6), f_1(6)
- 10095923 to 10095923 labelled g_1(6), f_1(6)
- 10095924 to 10095919 labelled active_1(5)
- 10095924 to 10095921 labelled active_1(5)
- 10095924 to 10095924 labelled g_1(5), f_1(5)
- 10095924 to 10095925 labelled f_1(6), g_1(6)
- 10095924 to 10095923 labelled active_1(5)
- 10095925 to 10095919 labelled active_1(6)
- 10095925 to 10095921 labelled active_1(6)
- 10095925 to 10095923 labelled active_1(6)
- 10095925 to 10095924 labelled g_1(5), f_1(5)
- 10095925 to 10095926 labelled f_1(7), g_1(7)
- 10095925 to 10095925 labelled f_1(6), g_1(6)
- 10095926 to 10095921 labelled active_1(7)
- 10095926 to 10095923 labelled active_1(7)
- 10095926 to 10095926 labelled f_1(7), g_1(7)
- 10095926 to 10095925 labelled f_1(6), g_1(6)