(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(f(X)) → f(active(X))
f(mark(X)) → mark(f(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:
8290936, 8290937, 8290938, 8290940, 8290941, 8290939, 8290942, 8290943, 8290944, 8290945, 8290946, 8290947, 8290949, 8290950, 8290951, 8290948, 8290952, 8290953, 8290954, 8290955, 8290956, 8290957, 8290958, 8290959, 8290960, 8290961, 8290962, 8290963, 8290964, 8290965, 8290966, 8290967, 8290968, 8290969, 8290970, 8290971, 8290972, 8290973, 8290974, 8290975, 8290976, 8290977, 8290978, 8290979, 8290980, 8290981, 8290982, 8290983, 8290984, 8290985, 8290986, 8290987, 8290988, 8290989
Node 8290936 is start node and node 8290937 is final node.
Those nodes are connect through the following edges:
- 8290936 to 8290938 labelled ok_1(0), mark_1(0)
- 8290936 to 8290939 labelled mark_1(0)
- 8290936 to 8290943 labelled top_1(0), g_1(0), f_1(0)
- 8290936 to 8290944 labelled f_1(0), top_1(0)
- 8290936 to 8290942 labelled ok_1(0)
- 8290936 to 8290953 labelled ok_1(1)
- 8290936 to 8290954 labelled top_1(1)
- 8290936 to 8290955 labelled mark_1(1)
- 8290936 to 8290966 labelled top_1(2)
- 8290936 to 8290983 labelled top_1(3)
- 8290937 to 8290937 labelled #_1(0)
- 8290938 to 8290937 labelled g_1(0), f_1(0)
- 8290938 to 8290945 labelled ok_1(1), mark_1(1)
- 8290940 to 8290941 labelled g_1(0)
- 8290941 to 8290942 labelled f_1(0)
- 8290939 to 8290940 labelled f_1(0)
- 8290942 to 8290937 labelled a(0)
- 8290943 to 8290937 labelled proper_1(0)
- 8290943 to 8290946 labelled g_1(1), f_1(1)
- 8290943 to 8290947 labelled ok_1(1)
- 8290943 to 8290957 labelled ok_1(2)
- 8290944 to 8290937 labelled active_1(0)
- 8290944 to 8290948 labelled mark_1(1)
- 8290944 to 8290952 labelled f_1(1)
- 8290944 to 8290956 labelled mark_1(2)
- 8290945 to 8290937 labelled f_1(1), g_1(1)
- 8290945 to 8290945 labelled ok_1(1), mark_1(1)
- 8290946 to 8290937 labelled proper_1(1)
- 8290946 to 8290946 labelled g_1(1), f_1(1)
- 8290946 to 8290947 labelled ok_1(1)
- 8290946 to 8290957 labelled ok_1(2)
- 8290947 to 8290937 labelled a(1)
- 8290949 to 8290950 labelled g_1(1)
- 8290950 to 8290951 labelled f_1(1)
- 8290951 to 8290937 labelled a(1)
- 8290948 to 8290949 labelled f_1(1)
- 8290952 to 8290937 labelled active_1(1)
- 8290952 to 8290948 labelled mark_1(1)
- 8290952 to 8290952 labelled f_1(1)
- 8290952 to 8290956 labelled mark_1(2)
- 8290953 to 8290947 labelled g_1(1), f_1(1)
- 8290953 to 8290957 labelled g_1(1), f_1(1)
- 8290954 to 8290947 labelled active_1(1)
- 8290954 to 8290948 labelled proper_1(1)
- 8290954 to 8290958 labelled f_1(2)
- 8290954 to 8290957 labelled active_1(1)
- 8290954 to 8290956 labelled proper_1(1)
- 8290954 to 8290961 labelled mark_1(2)
- 8290954 to 8290969 labelled mark_1(3)
- 8290954 to 8290970 labelled mark_1(3)
- 8290954 to 8290973 labelled ok_1(3)
- 8290955 to 8290948 labelled f_1(1)
- 8290955 to 8290956 labelled f_1(1)
- 8290956 to 8290948 labelled f_1(2)
- 8290956 to 8290956 labelled f_1(2)
- 8290957 to 8290947 labelled f_1(2), g_1(2)
- 8290957 to 8290957 labelled f_1(2), g_1(2)
- 8290958 to 8290949 labelled proper_1(2)
- 8290958 to 8290959 labelled g_1(2)
- 8290958 to 8290948 labelled proper_1(2)
- 8290958 to 8290957 labelled active_1(2)
- 8290958 to 8290956 labelled proper_1(2)
- 8290958 to 8290947 labelled active_1(2)
- 8290958 to 8290965 labelled f_1(3)
- 8290958 to 8290958 labelled f_1(2)
- 8290958 to 8290961 labelled mark_1(2)
- 8290958 to 8290969 labelled mark_1(3)
- 8290958 to 8290970 labelled mark_1(3)
- 8290958 to 8290972 labelled ok_1(3)
- 8290958 to 8290973 labelled ok_1(3)
- 8290958 to 8290974 labelled mark_1(4)
- 8290958 to 8290977 labelled ok_1(4)
- 8290959 to 8290950 labelled proper_1(2)
- 8290959 to 8290960 labelled f_1(2)
- 8290959 to 8290967 labelled ok_1(3)
- 8290960 to 8290951 labelled proper_1(2)
- 8290960 to 8290964 labelled ok_1(2)
- 8290961 to 8290962 labelled f_1(2)
- 8290962 to 8290963 labelled g_1(2)
- 8290963 to 8290964 labelled f_1(2)
- 8290964 to 8290937 labelled a(2)
- 8290965 to 8290948 labelled proper_1(3)
- 8290965 to 8290957 labelled active_1(3)
- 8290965 to 8290956 labelled proper_1(3)
- 8290965 to 8290947 labelled active_1(3)
- 8290965 to 8290965 labelled f_1(3)
- 8290965 to 8290958 labelled f_1(2)
- 8290965 to 8290961 labelled mark_1(2)
- 8290965 to 8290970 labelled mark_1(3)
- 8290965 to 8290969 labelled mark_1(3)
- 8290965 to 8290973 labelled ok_1(3)
- 8290965 to 8290974 labelled mark_1(4)
- 8290965 to 8290977 labelled ok_1(4)
- 8290966 to 8290961 labelled proper_1(2)
- 8290966 to 8290968 labelled f_1(3)
- 8290966 to 8290969 labelled proper_1(2)
- 8290966 to 8290970 labelled proper_1(2)
- 8290966 to 8290973 labelled active_1(2)
- 8290966 to 8290982 labelled ok_1(4)
- 8290967 to 8290964 labelled f_1(3)
- 8290968 to 8290962 labelled proper_1(3)
- 8290968 to 8290971 labelled g_1(3)
- 8290968 to 8290961 labelled proper_1(3)
- 8290968 to 8290969 labelled proper_1(3)
- 8290968 to 8290970 labelled proper_1(3)
- 8290968 to 8290968 labelled f_1(3)
- 8290968 to 8290973 labelled active_1(3)
- 8290968 to 8290972 labelled active_1(3)
- 8290968 to 8290979 labelled f_1(4)
- 8290968 to 8290974 labelled proper_1(3)
- 8290968 to 8290977 labelled active_1(3)
- 8290968 to 8290981 labelled ok_1(4)
- 8290968 to 8290982 labelled ok_1(4)
- 8290968 to 8290984 labelled ok_1(5)
- 8290969 to 8290961 labelled f_1(3)
- 8290970 to 8290969 labelled f_1(3)
- 8290970 to 8290970 labelled f_1(3)
- 8290970 to 8290974 labelled f_1(3)
- 8290971 to 8290963 labelled proper_1(3)
- 8290971 to 8290975 labelled f_1(3)
- 8290971 to 8290978 labelled ok_1(4)
- 8290972 to 8290967 labelled g_1(3)
- 8290973 to 8290972 labelled f_1(3)
- 8290973 to 8290973 labelled f_1(3)
- 8290973 to 8290977 labelled f_1(3)
- 8290974 to 8290969 labelled f_1(4)
- 8290974 to 8290970 labelled f_1(4)
- 8290974 to 8290974 labelled f_1(4)
- 8290975 to 8290964 labelled proper_1(3)
- 8290975 to 8290976 labelled ok_1(3)
- 8290976 to 8290937 labelled a(3)
- 8290977 to 8290973 labelled f_1(4)
- 8290977 to 8290977 labelled f_1(4)
- 8290978 to 8290976 labelled f_1(4)
- 8290979 to 8290969 labelled proper_1(4)
- 8290979 to 8290974 labelled proper_1(4)
- 8290979 to 8290961 labelled proper_1(4)
- 8290979 to 8290970 labelled proper_1(4)
- 8290979 to 8290973 labelled active_1(4)
- 8290979 to 8290979 labelled f_1(4)
- 8290979 to 8290968 labelled f_1(3)
- 8290979 to 8290980 labelled f_1(5)
- 8290979 to 8290977 labelled active_1(4)
- 8290979 to 8290972 labelled active_1(4)
- 8290979 to 8290982 labelled ok_1(4)
- 8290979 to 8290984 labelled ok_1(5)
- 8290979 to 8290986 labelled ok_1(6)
- 8290980 to 8290974 labelled proper_1(5)
- 8290980 to 8290969 labelled proper_1(5)
- 8290980 to 8290970 labelled proper_1(5)
- 8290980 to 8290979 labelled f_1(4)
- 8290980 to 8290977 labelled active_1(5)
- 8290980 to 8290973 labelled active_1(5)
- 8290980 to 8290980 labelled f_1(5)
- 8290980 to 8290984 labelled ok_1(5)
- 8290980 to 8290986 labelled ok_1(6)
- 8290981 to 8290978 labelled g_1(4)
- 8290982 to 8290981 labelled f_1(4)
- 8290982 to 8290982 labelled f_1(4)
- 8290982 to 8290984 labelled f_1(4)
- 8290983 to 8290982 labelled active_1(3)
- 8290983 to 8290985 labelled f_1(4)
- 8290984 to 8290982 labelled f_1(5)
- 8290984 to 8290984 labelled f_1(5)
- 8290984 to 8290986 labelled f_1(5)
- 8290985 to 8290981 labelled active_1(4)
- 8290985 to 8290982 labelled active_1(4)
- 8290985 to 8290987 labelled f_1(5)
- 8290985 to 8290984 labelled active_1(4)
- 8290986 to 8290984 labelled f_1(6)
- 8290986 to 8290986 labelled f_1(6)
- 8290987 to 8290981 labelled active_1(5)
- 8290987 to 8290984 labelled active_1(5)
- 8290987 to 8290982 labelled active_1(5)
- 8290987 to 8290987 labelled f_1(5)
- 8290987 to 8290988 labelled f_1(6)
- 8290987 to 8290986 labelled active_1(5)
- 8290988 to 8290984 labelled active_1(6)
- 8290988 to 8290982 labelled active_1(6)
- 8290988 to 8290986 labelled active_1(6)
- 8290988 to 8290987 labelled f_1(5)
- 8290988 to 8290989 labelled f_1(7)
- 8290988 to 8290988 labelled f_1(6)
- 8290989 to 8290986 labelled active_1(7)
- 8290989 to 8290984 labelled active_1(7)
- 8290989 to 8290989 labelled f_1(7)
- 8290989 to 8290988 labelled f_1(6)