(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(f(g(f(a))))
active(g(X)) → g(active(X))
g(mark(X)) → mark(g(X))
proper(f(X)) → f(proper(X))
proper(a) → ok(a)
proper(g(X)) → g(proper(X))
f(ok(X)) → ok(f(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:
492923, 492924, 492925, 492926, 492927, 492928, 492929, 492930, 492931, 492932, 492933, 492934, 492935, 492936, 492937, 492939, 492938, 492940, 492941, 492942, 492943, 492944, 492945, 492946, 492947, 492948, 492949, 492950, 492952, 492951, 492953, 492954, 492955, 492956, 492957, 492958, 492959, 492960, 492961, 492962, 492963, 492964, 492965, 492966, 492967, 492968, 492969, 492970, 492971, 492972, 492973, 492974, 492975, 492976, 492977
Node 492923 is start node and node 492924 is final node.
Those nodes are connect through the following edges:
- 492923 to 492925 labelled g_1(0), top_1(0)
- 492923 to 492926 labelled ok_1(0), mark_1(0)
- 492923 to 492927 labelled mark_1(0)
- 492923 to 492931 labelled top_1(0), g_1(0), f_1(0)
- 492923 to 492930 labelled ok_1(0)
- 492923 to 492940 labelled top_1(1)
- 492923 to 492941 labelled mark_1(1)
- 492923 to 492942 labelled ok_1(1)
- 492923 to 492954 labelled top_1(2)
- 492923 to 492972 labelled top_1(3)
- 492924 to 492924 labelled #_1(0)
- 492925 to 492924 labelled active_1(0)
- 492925 to 492935 labelled g_1(1)
- 492925 to 492936 labelled mark_1(1)
- 492925 to 492944 labelled mark_1(2)
- 492926 to 492924 labelled g_1(0), f_1(0)
- 492926 to 492934 labelled ok_1(1), mark_1(1)
- 492927 to 492928 labelled f_1(0)
- 492928 to 492929 labelled g_1(0)
- 492929 to 492930 labelled f_1(0)
- 492930 to 492924 labelled a(0)
- 492931 to 492924 labelled proper_1(0)
- 492931 to 492932 labelled g_1(1), f_1(1)
- 492931 to 492933 labelled ok_1(1)
- 492931 to 492945 labelled ok_1(2)
- 492932 to 492924 labelled proper_1(1)
- 492932 to 492932 labelled g_1(1), f_1(1)
- 492932 to 492933 labelled ok_1(1)
- 492932 to 492945 labelled ok_1(2)
- 492933 to 492924 labelled a(1)
- 492934 to 492924 labelled f_1(1), g_1(1)
- 492934 to 492934 labelled ok_1(1), mark_1(1)
- 492935 to 492924 labelled active_1(1)
- 492935 to 492935 labelled g_1(1)
- 492935 to 492936 labelled mark_1(1)
- 492935 to 492944 labelled mark_1(2)
- 492936 to 492937 labelled f_1(1)
- 492937 to 492938 labelled g_1(1)
- 492939 to 492924 labelled a(1)
- 492938 to 492939 labelled f_1(1)
- 492940 to 492936 labelled proper_1(1)
- 492940 to 492933 labelled active_1(1)
- 492940 to 492943 labelled f_1(2)
- 492940 to 492945 labelled active_1(1)
- 492940 to 492944 labelled proper_1(1)
- 492940 to 492947 labelled g_1(2)
- 492940 to 492949 labelled mark_1(2)
- 492940 to 492956 labelled mark_1(3)
- 492940 to 492960 labelled ok_1(3)
- 492941 to 492936 labelled g_1(1)
- 492941 to 492944 labelled g_1(1)
- 492942 to 492933 labelled g_1(1), f_1(1)
- 492942 to 492945 labelled f_1(1), g_1(1)
- 492943 to 492937 labelled proper_1(2)
- 492943 to 492946 labelled g_1(2)
- 492943 to 492959 labelled ok_1(3)
- 492944 to 492936 labelled g_1(2)
- 492944 to 492944 labelled g_1(2)
- 492945 to 492933 labelled g_1(2), f_1(2)
- 492945 to 492945 labelled g_1(2), f_1(2)
- 492946 to 492938 labelled proper_1(2)
- 492946 to 492948 labelled f_1(2)
- 492946 to 492957 labelled ok_1(3)
- 492947 to 492945 labelled active_1(2)
- 492947 to 492933 labelled active_1(2)
- 492947 to 492944 labelled proper_1(2)
- 492947 to 492936 labelled proper_1(2)
- 492947 to 492953 labelled g_1(3)
- 492947 to 492943 labelled f_1(2)
- 492947 to 492949 labelled mark_1(2)
- 492947 to 492956 labelled mark_1(3)
- 492947 to 492960 labelled ok_1(3)
- 492947 to 492962 labelled mark_1(4)
- 492947 to 492965 labelled ok_1(4)
- 492948 to 492939 labelled proper_1(2)
- 492948 to 492952 labelled ok_1(2)
- 492949 to 492950 labelled f_1(2)
- 492950 to 492951 labelled g_1(2)
- 492952 to 492924 labelled a(2)
- 492951 to 492952 labelled f_1(2)
- 492953 to 492945 labelled active_1(3)
- 492953 to 492933 labelled active_1(3)
- 492953 to 492944 labelled proper_1(3)
- 492953 to 492936 labelled proper_1(3)
- 492953 to 492953 labelled g_1(3)
- 492953 to 492943 labelled f_1(2)
- 492953 to 492949 labelled mark_1(2)
- 492953 to 492956 labelled mark_1(3)
- 492953 to 492960 labelled ok_1(3)
- 492953 to 492962 labelled mark_1(4)
- 492953 to 492965 labelled ok_1(4)
- 492954 to 492949 labelled proper_1(2)
- 492954 to 492955 labelled f_1(3)
- 492954 to 492956 labelled proper_1(2)
- 492954 to 492961 labelled g_1(3)
- 492954 to 492960 labelled active_1(2)
- 492954 to 492970 labelled ok_1(4)
- 492955 to 492950 labelled proper_1(3)
- 492955 to 492958 labelled g_1(3)
- 492955 to 492968 labelled ok_1(4)
- 492956 to 492949 labelled g_1(3)
- 492956 to 492956 labelled g_1(3)
- 492956 to 492962 labelled g_1(3)
- 492957 to 492952 labelled f_1(3)
- 492958 to 492951 labelled proper_1(3)
- 492958 to 492963 labelled f_1(3)
- 492958 to 492967 labelled ok_1(4)
- 492959 to 492957 labelled g_1(3)
- 492960 to 492959 labelled f_1(3)
- 492960 to 492960 labelled g_1(3)
- 492960 to 492965 labelled g_1(3)
- 492961 to 492949 labelled proper_1(3)
- 492961 to 492956 labelled proper_1(3)
- 492961 to 492955 labelled f_1(3)
- 492961 to 492966 labelled g_1(4)
- 492961 to 492962 labelled proper_1(3)
- 492961 to 492960 labelled active_1(3)
- 492961 to 492965 labelled active_1(3)
- 492961 to 492970 labelled ok_1(4)
- 492961 to 492971 labelled ok_1(5)
- 492962 to 492956 labelled g_1(4)
- 492962 to 492962 labelled g_1(4)
- 492963 to 492952 labelled proper_1(3)
- 492963 to 492964 labelled ok_1(3)
- 492964 to 492924 labelled a(3)
- 492965 to 492960 labelled g_1(4)
- 492965 to 492965 labelled g_1(4)
- 492966 to 492962 labelled proper_1(4)
- 492966 to 492956 labelled proper_1(4)
- 492966 to 492949 labelled proper_1(4)
- 492966 to 492955 labelled f_1(3)
- 492966 to 492960 labelled active_1(4)
- 492966 to 492966 labelled g_1(4)
- 492966 to 492969 labelled g_1(5)
- 492966 to 492965 labelled active_1(4)
- 492966 to 492970 labelled ok_1(4)
- 492966 to 492971 labelled ok_1(5)
- 492966 to 492974 labelled ok_1(6)
- 492967 to 492964 labelled f_1(4)
- 492968 to 492967 labelled g_1(4)
- 492969 to 492956 labelled proper_1(5)
- 492969 to 492962 labelled proper_1(5)
- 492969 to 492960 labelled active_1(5)
- 492969 to 492966 labelled g_1(4)
- 492969 to 492965 labelled active_1(5)
- 492969 to 492969 labelled g_1(5)
- 492969 to 492971 labelled ok_1(5)
- 492969 to 492974 labelled ok_1(6)
- 492970 to 492968 labelled f_1(4)
- 492970 to 492970 labelled g_1(4)
- 492970 to 492971 labelled g_1(4)
- 492971 to 492970 labelled g_1(5)
- 492971 to 492971 labelled g_1(5)
- 492971 to 492974 labelled g_1(5)
- 492972 to 492970 labelled active_1(3)
- 492972 to 492973 labelled g_1(4)
- 492973 to 492970 labelled active_1(4)
- 492973 to 492975 labelled g_1(5)
- 492973 to 492971 labelled active_1(4)
- 492974 to 492971 labelled g_1(6)
- 492974 to 492974 labelled g_1(6)
- 492975 to 492970 labelled active_1(5)
- 492975 to 492971 labelled active_1(5)
- 492975 to 492975 labelled g_1(5)
- 492975 to 492976 labelled g_1(6)
- 492975 to 492974 labelled active_1(5)
- 492976 to 492971 labelled active_1(6)
- 492976 to 492970 labelled active_1(6)
- 492976 to 492974 labelled active_1(6)
- 492976 to 492977 labelled g_1(7)
- 492976 to 492975 labelled g_1(5)
- 492976 to 492976 labelled g_1(6)
- 492977 to 492974 labelled active_1(7)
- 492977 to 492971 labelled active_1(7)
- 492977 to 492977 labelled g_1(7)
- 492977 to 492976 labelled g_1(6)