YES We show the termination of the TRS R: active(f(x)) -> mark(f(f(x))) chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) mat(f(x),f(y())) -> f(mat(x,y())) chk(no(c())) -> active(c()) mat(f(x),c()) -> no(c()) f(active(x)) -> active(f(x)) f(no(x)) -> no(f(x)) f(mark(x)) -> mark(f(x)) tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(f(x)) -> f#(f(x)) p2: chk#(no(f(x))) -> f#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) p3: chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) p4: chk#(no(f(x))) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) p5: chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) p6: chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(f(X()))))))))) p7: chk#(no(f(x))) -> f#(f(f(f(f(f(f(f(X())))))))) p8: chk#(no(f(x))) -> f#(f(f(f(f(f(f(X()))))))) p9: chk#(no(f(x))) -> f#(f(f(f(f(f(X())))))) p10: chk#(no(f(x))) -> f#(f(f(f(f(X()))))) p11: chk#(no(f(x))) -> f#(f(f(f(X())))) p12: chk#(no(f(x))) -> f#(f(f(X()))) p13: chk#(no(f(x))) -> f#(f(X())) p14: chk#(no(f(x))) -> f#(X()) p15: mat#(f(x),f(y())) -> f#(mat(x,y())) p16: mat#(f(x),f(y())) -> mat#(x,y()) p17: chk#(no(c())) -> active#(c()) p18: f#(active(x)) -> active#(f(x)) p19: f#(active(x)) -> f#(x) p20: f#(no(x)) -> f#(x) p21: f#(mark(x)) -> f#(x) p22: tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) p23: tp#(mark(x)) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) p24: tp#(mark(x)) -> mat#(f(f(f(f(f(f(f(f(f(f(X())))))))))),x) p25: tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(f(X())))))))))) p26: tp#(mark(x)) -> f#(f(f(f(f(f(f(f(f(X()))))))))) p27: tp#(mark(x)) -> f#(f(f(f(f(f(f(f(X())))))))) p28: tp#(mark(x)) -> f#(f(f(f(f(f(f(X()))))))) p29: tp#(mark(x)) -> f#(f(f(f(f(f(X())))))) p30: tp#(mark(x)) -> f#(f(f(f(f(X()))))) p31: tp#(mark(x)) -> f#(f(f(f(X())))) p32: tp#(mark(x)) -> f#(f(f(X()))) p33: tp#(mark(x)) -> f#(f(X())) p34: tp#(mark(x)) -> f#(X()) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The estimated dependency graph contains the following SCCs: {p22} {p3} {p1, p18, p19, p20, p21} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: tp#(mark(x)) -> tp#(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r1, r2, r3, r4, r5, r6, r7, r8, r9 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: max/plus interpretation on natural numbers: tp#_A(x1) = max{1, x1 - 10} mark_A(x1) = max{12, x1 - 7} chk_A(x1) = max{12, x1 - 12} mat_A(x1,x2) = max{4, x1 - 1, x2 - 4} f_A(x1) = max{5, x1} X_A = 0 active_A(x1) = max{12, x1 - 6} no_A(x1) = max{4, x1 - 2} y_A = 9 c_A = 3 tp_A(x1) = max{3, x1 - 18} base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: tp#_A(x1) = max{0, x1 - 81} mark_A(x1) = max{80, x1 - 25} chk_A(x1) = max{5, x1 - 476} mat_A(x1,x2) = max{533, x1 - 17, x2 - 3} f_A(x1) = x1 + 36 X_A = 3 active_A(x1) = x1 + 57 no_A(x1) = x1 + 533 y_A = 1015 c_A = 0 tp_A(x1) = x1 + 362 tp#!_A(x1) = x1 + 70 mark!_A(x1) = max{26, x1 - 59} chk!_A(x1) = max{59, x1 - 1046} mat!_A(x1,x2) = max{1015, x1 - 51} f!_A(x1) = max{6, x1 + 2} X!_A = 6 active!_A(x1) = max{6, x1 + 5} no!_A(x1) = max{1, x1 - 1086} y!_A = 1016 c!_A = 6 tp!_A(x1) = max{25, x1 - 115} partial status: pi(tp#) = [] pi(mark) = [] pi(chk) = [] pi(mat) = [] pi(f) = [] pi(X) = [] pi(active) = [] pi(no) = [] pi(y) = [] pi(c) = [] pi(tp) = [] The following rules are removed: p1 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: chk#(no(f(x))) -> chk#(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x)) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r3, r5 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: max/plus interpretation on natural numbers: chk#_A(x1) = 13 no_A(x1) = max{15, x1 - 78} f_A(x1) = max{16, x1 - 16} mat_A(x1,x2) = x2 + 26 X_A = 12 y_A = 15 c_A = 3 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: chk#_A(x1) = 0 no_A(x1) = max{77, x1 - 113} f_A(x1) = max{196, x1 - 5} mat_A(x1,x2) = max{82, x1 - 197, x2 - 121} X_A = 203 y_A = 322 c_A = 122 chk#!_A(x1) = x1 + 120 no!_A(x1) = max{206, x1 - 123} f!_A(x1) = max{204, x1 - 252} mat!_A(x1,x2) = 72 X!_A = 205 y!_A = 71 c!_A = 202 partial status: pi(chk#) = [] pi(no) = [] pi(f) = [] pi(mat) = [] pi(X) = [] pi(y) = [] pi(c) = [] The following rules are removed: p1 Then no dependency pair remains. -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(f(x)) -> f#(f(x)) p2: f#(mark(x)) -> f#(x) p3: f#(no(x)) -> f#(x) p4: f#(active(x)) -> f#(x) p5: f#(active(x)) -> active#(f(x)) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r1, r5, r6, r7, r8 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: max/plus interpretation on natural numbers: active#_A(x1) = max{3, x1 - 15} f_A(x1) = max{10, x1} f#_A(x1) = max{3, x1 - 24} mark_A(x1) = max{22, x1 + 2} no_A(x1) = max{28, x1 + 2} active_A(x1) = max{23, x1 + 11} mat_A(x1,x2) = max{59, x1 + 49, x2 - 11} c_A = 9 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: active#_A(x1) = max{0, x1 - 4} f_A(x1) = max{3, x1 - 12} f#_A(x1) = max{0, x1 - 4} mark_A(x1) = max{1, x1} no_A(x1) = max{3, x1} active_A(x1) = x1 mat_A(x1,x2) = max{11, x1 - 93, x2 - 95} c_A = 3 active#!_A(x1) = x1 + 1 f!_A(x1) = 8 f#!_A(x1) = max{4, x1 - 4} mark!_A(x1) = max{5, x1 + 1} no!_A(x1) = 7 active!_A(x1) = max{5, x1 - 4} mat!_A(x1,x2) = max{0, x2 - 4} c!_A = 1 partial status: pi(active#) = [] pi(f) = [1] pi(f#) = [] pi(mark) = [] pi(no) = [1] pi(active) = [] pi(mat) = [1] pi(c) = [] The following rules are removed: p3 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(f(x)) -> f#(f(x)) p2: f#(mark(x)) -> f#(x) p3: f#(active(x)) -> f#(x) p4: f#(active(x)) -> active#(f(x)) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The estimated dependency graph contains the following SCCs: {p1, p2, p3, p4} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(f(x)) -> f#(f(x)) p2: f#(active(x)) -> active#(f(x)) p3: f#(active(x)) -> f#(x) p4: f#(mark(x)) -> f#(x) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r1, r5, r6, r7, r8 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: max/plus interpretation on natural numbers: active#_A(x1) = max{4, x1 - 19} f_A(x1) = x1 + 14 f#_A(x1) = max{4, x1 - 19} active_A(x1) = x1 + 19 mark_A(x1) = max{24, x1 + 3} mat_A(x1,x2) = max{125, x1 - 15, x2 - 2} c_A = 1 no_A(x1) = x1 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: active#_A(x1) = max{0, x1 - 32} f_A(x1) = max{31, x1 - 33} f#_A(x1) = max{0, x1 - 32} active_A(x1) = max{30, x1} mark_A(x1) = x1 mat_A(x1,x2) = max{31, x1 - 48, x2 - 50} c_A = 46 no_A(x1) = max{3, x1 - 47} active#!_A(x1) = max{2, x1 - 28} f!_A(x1) = max{5, x1 - 22} f#!_A(x1) = max{3, x1 - 61} active!_A(x1) = max{6, x1 - 61} mark!_A(x1) = max{4, x1 - 60} mat!_A(x1,x2) = max{2, x1 - 38, x2 - 300} c!_A = 1 no!_A(x1) = 5 partial status: pi(active#) = [] pi(f) = [] pi(f#) = [] pi(active) = [] pi(mark) = [1] pi(mat) = [] pi(c) = [] pi(no) = [] The following rules are removed: p4 -- SCC decomposition. Consider the dependency pair problem (P, R), where P consists of p1: active#(f(x)) -> f#(f(x)) p2: f#(active(x)) -> active#(f(x)) p3: f#(active(x)) -> f#(x) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The estimated dependency graph contains the following SCCs: {p1, p2, p3} -- Reduction pair. Consider the dependency pair problem (P, R), where P consists of p1: active#(f(x)) -> f#(f(x)) p2: f#(active(x)) -> f#(x) p3: f#(active(x)) -> active#(f(x)) and R consists of: r1: active(f(x)) -> mark(f(f(x))) r2: chk(no(f(x))) -> f(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) r3: mat(f(x),f(y())) -> f(mat(x,y())) r4: chk(no(c())) -> active(c()) r5: mat(f(x),c()) -> no(c()) r6: f(active(x)) -> active(f(x)) r7: f(no(x)) -> no(f(x)) r8: f(mark(x)) -> mark(f(x)) r9: tp(mark(x)) -> tp(chk(mat(f(f(f(f(f(f(f(f(f(f(X())))))))))),x))) The set of usable rules consists of r1, r5, r6, r7, r8 Take the reduction pair: generalized weighted path order (>=MG, >G) base order 1: max/plus interpretation on natural numbers: active#_A(x1) = x1 + 6 f_A(x1) = x1 + 7 f#_A(x1) = max{3, x1 - 8} active_A(x1) = x1 + 22 mark_A(x1) = 10 mat_A(x1,x2) = max{163, x1 - 19, x2 - 163} c_A = 162 no_A(x1) = 112 base order 2: marked-algebra reduction triple (>=A, >=A!, >A!): max/plus interpretation on natural numbers: active#_A(x1) = 1 f_A(x1) = max{261, x1 - 40} f#_A(x1) = 1 active_A(x1) = max{39, x1 - 40} mark_A(x1) = max{28, x1 - 298} mat_A(x1,x2) = max{39, x1 - 237, x2 - 296} c_A = 0 no_A(x1) = 1 active#!_A(x1) = x1 + 41 f!_A(x1) = 4 f#!_A(x1) = x1 + 343 active!_A(x1) = 0 mark!_A(x1) = max{2, x1 - 262} mat!_A(x1,x2) = max{6, x1 - 284, x2 - 326} c!_A = 5 no!_A(x1) = max{4, x1 - 325} partial status: pi(active#) = [1] pi(f) = [1] pi(f#) = [] pi(active) = [] pi(mark) = [] pi(mat) = [] pi(c) = [] pi(no) = [] The following rules are removed: p1, p2, p3 Then no dependency pair remains.